Safe and secure software-defined networks in P4
The project goal is to develop new methods and tools to verify the correctness of Software-Defined Networking (SDN) configurations. Modern SDN-enabled network routers and switches are programmable using vendor-neutral languages and standards (such as P4), hence they are very powerful and flexible. Unfortunately, this power and flexibility comes at a cost: SDN configurations can be complicated, and mistakes can be costly - very simple bugs can bring whole networks and businesses offline, or compromise their privacy and security. Therefore, our research question is: can we prevent these mistakes? Can we verify the correctness of SDN configurations before they are deployed?
Further information is available
here or by contacting associate professor
Alceste Scalas.
Automated Verification of Sensitivity Properties for Probabilistic Programs
Sensitivity measures how much program outputs vary when changing inputs. We propose exploring novel methodologies for specifying and verifying sensitivity properties of probabilistic programs such that they (a) are comprehensible to everyday programmers, (b) can be verified using automated theorem provers, and (c) cover properties from the machine learning and security literature. The overall objective of the project is to explore how automated verification of sensitivity properties of probabilistic programs can support developers in increasing the trust in their software through formal assurances.
LIRA - Live Road Assessment
LiRA project will enable data from sensors to be collected in regular passenger cars and develop associated models to assess road condition. Road wear can thus be detected and improved much earlier, enabling the roads to be maintained more efficiently - and for fewer resources. Modern cars are equipped with a variety of sensors that collect a lot of different data while driving. This data can - directly or indirectly - be related to the condition of the specific road on which the car is travelling.
Further information is available
here or by contacting associate professor
Ekkart Kindler.
Sb3D - Security by Design in Digital Denmark
Software is becoming the engine of business operations. Therefore, it is crucial that software solutions are secure. Small and medium software companies need more knowledge and better tools to strengthen the security of their solutions. The project Security by Design in Digital Denmark (Sb3D) aims at ensuring that Security by Design (SbD) is the norm for software developed in Denmark.
SIOT – Secure Internet of Things – Risk analysis in design and operation
SIOT will develop a modelling formalism with automated tool support, for performing such risk assessments and allowing for extensive “what‐if” scenario analysis. The starting point will be the well‐ known and widely used formalism of attack‐defense trees extended to include various quantities, e.g., cost or energy consumption, as well as game features, for modelling collaboration and competition between systems and between a system and its environment.
Further information is available here or by contacting associate professor Alberto Lluch Lafuente.
CyberSec4Europe
CyberSec4Europe is a research-based consortium with 43 participants from 22 EU Member States and Associated Countries. As a pilot for a Cybersecurity Competence Network, it will test and demonstrate potential governance structures for the network of competence centres using the best practice examples from the expertise and experience of the participants, including concepts like CERN.
Further information is available at cybersec4europe.eu/ or by contacting associate professor Alberto Lluch Lafuente.
LIGHTest
The objective of LIGHTest is to create a global cross-domain trust infrastructure that renders it transparent and easy for verifiers to evaluate electronic transactions. By querying different trust authorities world-wide and combining trust aspects related to identity, business, reputation etc. it will become possible to conduct domain-specific trust decisions.
Further information is available at lightest.eu or by contacting associate professor Sebastian A. Mödersheim.
CompoSec
CompoSec is a A Sapere Aude research project whose goals are to develop: (1) Real-world Compositionality Results that are applicable to today's systems without modification -- instead of strong unrealistic assumptions; (2) A Unified Framework. Make explicit and order the diversity of existing compositionality results within a single general model with machine-checked proofs in the Isabelle theorem prover.
Tool Support; (3) A verifier that checks whether a given set of components satisfies the conditions for secure composition and suggests changes otherwise.
Further information is available here or by contacting associate professor Sebastian A. Mödersheim.
IDEA4CPS
IDEA4CPS is funded by the Danish Foundation for Basic Research and studies the foundations of cyber-physical systems. The aim is to research and develop mathematically well-founded and coherent models, methods, and tools that may serve as the foundation of a model-driven design methodology for cyber-physical systems.
Further information is available at IDEA4CPS.dk or by contacting professor Flemming Nielson.
TREsPASS
TREsPASS is a European integrated research project on Technology-supported Risk Estimation by Predictive Assessment of Socio-technical Security. Current risk management methods provide descriptive tools for assessing threats by systematic brainstorming. In today’s dynamic attack landscape, however, this process is too slow and exceeds the limits of human imaginative capability. Emerging security risks demand an extension of established methods with an analytical approach to predict, prioritise, and prevent complex attacks. The TREsPASS project develops quantitative and organisation-specific means to achieve this in complex socio-technical environments.
Further information is available at trespass-project.eu or by contacting associate professor Christian W. Probst.
FutureID: Shaping the Future of Electronic Identity
FutureID is a European integrated research project to build a comprehensive, flexible, privacy-aware and ubiquitously usable identity management infrastructure for Europe, which integrates existing eID technology and trust infrastructures, emerging federated identity management services and modern credential technologies to provide a user-centric system for the trustworthy and accountable management of identity claims. DTU and the academic partners will focus on the development of languages and methods for formally modeling, analyzing, and securely composing the identity systems.
Further information is available at futureid.eu or by contacting associate professor Sebastian A. Mödersheim.
MT-LAB: a VKR Centre of Excellence on Modelling of Information Technology
The goal of the research centre was to explore and develop methods for formal verification of modern advanced software systems. Such methods have already been successfully applied to self‐ contained and relatively simple systems. The aim of this project was to develop new methods and expand the applicability of previous methods in order to formally verify the functionality of complex interacting modern software systems. In the project recent theory and methods from computer science and mathematical modelling have been combined.
Further information is available by contacting professor Flemming Nielson.
SESAMO: Security and Safety Modelling
The SESAMO project addressed the root causes of problems arising with convergence of safety and security in embedded systems at the architectural level, where subtle and poorly understood interactions between functional safety and security mechanisms impede system definition, development, certification, and accreditation procedures and standards.
Further information is available at sesamo-project.eu by contacting professor Flemming Nielson.