Completed projects

Formalising computational soundness for protocol implementations

Read more on the project web page.

Foundations of Database Access Control

Read more on the project web page.

Access Control for Next Generation Systems

Read more on the project web page.

Secure Communication with Humans

Read more on the project web page.

Analyzing and Maintaining Access Control Infrastructures

An extension of access control policies that strikes a balance between expressiveness in policy specification and efficiency in policy analysis, methods for checking that before every security relevant section in the code, an authorization request is correctly sent to the PDP, and procedures for automatically mining attribute-based policies from access control matrices.

Read more on the project web page.

Secure Deletion and Data Deletion

We analyzed solutions to the problem of secure deletion: how to make sensitive data unaccessible from a storage medium. In particular we provide methods to securely delete data from modern devices working at different levels (user-space, log-structured filesystems, flash memory, etc.).

Read more on the project web page.

NESSoS

Network of Excellence on Engineering Secure Future Internet Software Services and Systems.

Read more on the project external pageweb pagecall_made.

SPACIOS

Secure Provision and Consumption in the Internet of Services.

Read more on the project external pageweb pagecall_made.

SPINACH

Security Protocol Improvement and Adversary Change.

Read more on the project web page.

Methods for the Design, Analysis, and Certification of Secure Boot Processes

In computer systems with layered architectures, the integrity of higher layers depends on the integrity of the lower layers and this chain begins with the boot process. The secure operation of the lowest-layer boot process is therefore an essential foundation for the integrity of the entire system. This requires the specification and verification of a security policy for the boot process.

Read more on the project web page.

DEPLOY

Industrial Deployment of System Engineering Methods.

DEPLOY is an European Commission external pageInformation and Communication Technologiescall_made FP7 project. The overall aim of the project is to make major advances in engineering methods for dependable systems through the deployment of formal engineering methods. The work of the project will be driven by the tasks of achieving and evaluating industrial take-up, initially by DEPLOY's industrial partners (Bosch, Siemens Transportation Systems, Space System Finland and SAP), of DEPLOY's methods and tools (external pageEvent-Bcall_made and the external pageRodin Platformcall_made), together with the necessary further research on these methods and tools.

Read more on the external pageproject web pagecall_made.

VerSePro

Verification of security and privacy protocols for wireless networks.

The objectives of this project are to provide MICS with a set of correctly proved security protocols along with methods and tool support for such verification.

Application: Mobile communications protocols of tomorrow are more secure.

The project's assets: A certain number of protocols will be developed, aiming at protecting location privacy of the "sensor internet", securing positioning in all-wireless networks and highly mobile ad hoc networks, as well as fostering cooperation between nodes.

New methods will be developed for the modelling and automated analysis of a wide spectrum of security protocols.

Model-based Testing of Security Policies

The goal of this project is to use security policies as model-based specifications and to derive test-cases for them. The policies are specified in Higher-order logic and we use HOL-TestGen, a test-case generator based on the theorem prover Isabelle/HOL to generate the test cases. This approach has already been applied to automatically generate test-cases for firewall policies - for both stateless and stateful firewalls.

Currently, we are investigating the security policies for a large-scale patient data-management system: the access framework for the National Program for IT in the NHS England (NPfIT). We focus on the policies governing access to the Summary Care Records held in the SPINE. Access to patient data in this system is governed by several concepts:

• Role-based Access Control
• Legitimate Relationships
• Patient's Consent
• Sealed Envelopes

The combination of these different concepts serves as a challenging scenario for model-based policy specification, policy analysis, and policy testing.

Read more on the HOL-TestGen external pageweb pagecall_made.

AVANTSSAR

Automated Validation of Trust and Security of Service Oriented Architectures.

Driven by rapidly changing requirements and business needs, IT systems and applications are undergoing a paradigm shift: components are replaced by services, distributed over the network, and composed and reconfigured dynamically in a demand-driven way into service-oriented architectures.

Exposing services in future network infrastructures entails a wide range of trust and security issues. Solving them is extremely hard since making the service components trustworthy is not sufficient: composing services leads to new subtle and dangerous vulnerabilities due to interference between component services and policies, the shared communication layer, and application functionality. Thus, one needs validation of both the service components and their composition into secure service architectures.

AVANTSSAR proposes a rigorous technology for the formal specification and Automated VAlidatioN of Trust and Security of Service-oriented ARchitectures. This technology will be automated into an integrated toolset, the AVANTSSAR Validation Platform, tuned on relevant industrial case studies.

The project develops:

• ASLan, the first formal language for specifying trust and security properties of services, their associated policies, and their composition into  service architectures.
• Automated techniques to reason about services, their dynamic composition, and their associated security policies into secure service architectures.
• The AVANTSSAR Validation Platform, an automated toolset for validating trust and security aspects of service-oriented architectures.
• A library of validated composed services and service architectures, proving that our technology scales to envisaged applications.

Migrating project results to industry and standardisation organisations will speed up the development of new network and service infrastructures, enhance their security and robustness, and increase the public acceptance of emerging IT systems and applications based on them.

Read more on the project external pageweb pagecall_made.

Role Mining

This project addresses an important practical problem in Information Security: developing and rationalizing access control infrastructures based on Role-Based Access Control (RBAC). RBAC is an approach for specifying user privileges for carrying out operations on system objects: Roles group together system privileges and users are assigned to roles, thereby granting them the associated privileges.
Although RBAC is conceptually simple, it is very difficult to configure RBAC systems in practice within large enterprises, i.e., to determine the appropriate roles and assign users to roles. This complexity leads to both high security administration costs and security weaknesses due to improperly implemented and administered security policies.

To tackle these problems, data mining techniques will be developed for both configuring RBAC systems and for assessing configurations. Data sets such as existing user privileges or job functions will be used for this analysis. The resulting configurations should satisfy various criteria such as minimizing the number of roles or minimizing the changes required when users are added to or removed from the system.

Read more on the project web page.

Usage Control in Ubiquitous Communication

The project started in 2009 and ended in 2011. It was carried out in collaboration with Nokia Research Center, Lausanne. Our objective in this project was to advance the state of the art in observing and controlling the usage of sensitive data in IT systems. We developed methods that monitor the use of data and ensure that usage is conform to the intended purposes for which the data was collected. Furthermore, based on these monitors, we designed and prototypically implemented architectures for pervasive computing applications that report on the misuse of sensitive data.

Read more on the project web page.

Information-Flow Security

Research in Information-Flow Security is concerned with investigating secrecy and integrity properties. It goes beyond studying access control in that it is concerned with the propagation of information in a system, and not only with its release. Information may propogate in unintended ways due to hidden channels where observers may gain information by examining different aspects of system behavior. One example of this is a so-called timing leak, through which a system reveals a secret by showing characteristic timing behavior. For example, a careless implementation of a cryptographic algorithm may reveal a user's secret key to a malicious party, even if that party can only observe the algorithm's running time. We are developing methods for detecting, quantifying, and eliminating information leaks, with a particular focus on timing leaks. Active avenues of research include the analysis of synchronous hardware and programming-language based methods for information flow analysis.

Formal Testing Techniques

Today, essentially two software verification techniques are used: formal software verification and software testing. Whereas formal verification is rarely used in "large-scale'' software developments, testing is widely used, but often in an ad-hoc manner. Recent research aims to systematize the foundations of testing and combine it with formal verification techniques such as theorem proving or model checking. Of particular interest are formal, specification-based testing techniques with respect to security-critical computer systems, for example firewalls or access-control mechanisms of web-services.

Specification-based Firewall Testing

(project funded by armasuisse)

Firewalls are a central component in network security. Nowadays everybody is using firewalls, unfortunately without having good means for determining if they are accomplishing their job correctly. The aim of this project is to develop a specification-based firewall testing methodology. The phrase "specification-based" is important here: firewalls in a bank have to accomplish a different goal than those in a university, thus we cannot use the same tests. Or said otherwise, for every environment we have to generate tests separately, based on the security policy of the respective environment.

Modelling and Verification in HOL-Z

The increasing complexity of today's software systems makes modeling an important phase during the software development process, both, on the level of requirement analysis and the system design. The ISO-standardized specification language Z can be used for a formal underpinning of these activities. In particular, the Z Method allows for relating Requirements and System Designs via formal refinement notions. In this project we are developing (on top of Isabelle/HOL) the interactive theorem prover environment HOL-Z that supports formal reasoning over Z specifications and formal proof on refinements. The system achieved meanwhile a reasonable degree of automation such that several substantial case studies (CVS Server, DARMA funded by Hitachi) had been realized, involving both refinement as well as temporal reasoning.

The increasing complexity of today's software systems makes modeling an important phase during the software development process, both, on the level of requirement analysis and the system design. The Unified Modeling Language (UML) has meanwhile achieved a remarkable acceptance in industrial projects of component-based, object-oriented systems. Further, the Object Constraint Language (OCL) has been proposed as a formal extension. OCL allows one to constrain UML models, e.g. by adding pre-conditions, post-conditions and invariants to class-diagrams. In this project we are developing (on top of Isabelle/HOL) the interactive theorem prover environment HOL-OCL that supports formal reasoning over UML/OCL specifications.