Computer security

Analysis of networked software

We study the impact of network communication delays and failures on the behavior of networked software, where error handling is difficult to test with conventional means.

Most software today communicates with other systems over a network. Networked systems are complex, and difficult to analyze because a networked system cannot be verified in isolation. We study the impact of network communication delays and failures on the behavior of networked software, where the impact of delays and connection loss are difficult to test with conventional means. Responsible:

Software security

Our research ranges from foundations to practice of software security with main focus on Language-Based Security and its applications to Web Security and IoT Security. We develop novel security models, defensive mechanisms, and tool support for finding and fixing software security vulnerabilities, as well as writing code that is secure by construction. Towards this end, we explore new technologies that lie at the intersection of computer security, programming languages, formal methods and software engineering.

Intelligence and security informatics

We study how systems, algorithms, and databases can be used for crisis management and homeland security related applications. In this domain, not only technical solutions but also the human ability to grasp the complexities of the threats, affect the level of success or failure. In our research, a particular interest is to help a decision-maker to gain so-called cyber situational awareness (CSA), requiring the use of different kinds of heterogeneous IT sensors (intrusion detection systems, web crawlers, a human observer, etc.) in order to obtain data to be fed to a data fusion process. Responsible:

Privacy

We are working toward privacy-preserving communication systems, mainly by decentralization and the development of privacy-enhancing technologies based on cryptography.

The last decade has seen an unprecedented growth of new services and applications for our lives online. Social networks, cloud computing, big data analysis, the Internet of Things, smart phones, homes, and metering offer many benefits. Along with the increased collection of online information that entails, our privacy has been declining. Both commercial entities and governments are tracking our behavior and data online. In our work, we aim to give control over their data and whom to share it with back to the individual rather than the service provider, also to strengthen democracy in the face of surveillance and censorship. Toward this end, we use cryptography and decentralization as our main tools for different aspects of privacy such as anonymity, deniability, and unlinkabilty along with security properties such as integrity and accountability. Some examples of this work include policy-hiding access control, privacy-preserving password authentication in completely decentralized systems, event organization, deniable messaging, and document submission systems. Responsible:

Provably secure systems

We study techniques and tools for modelling and analysis of low level security-critical system components such as operating systems, hypervisors, and the their underlying hardware.

Application security is critically dependent on the integrity of the underlying mechanisms at operating system and hardware level to ensure that keys can be kept private, that sensitive memory cannot be read, and so on. We study such low level security mechanisms, discover vulnerabilities in their implementation, and use formal methods such as theorem provers and program verifiers to model and analyse their behaviour. For instance we are currently verifying a hypervisor able to support Android together with several secure guests running on the ARMv8 multicore platform as used in contemporary smartphones from companies such as Apple, Samsung, Huawei, Sony. Responsible:

Provably secure systems

We design and formally verify secure low-level platforms to mathematically prove absence of illicit information flows, integrity of critical resources, and absence of code injection.

Security of low-level SW like operating systems and hypervisors is critical to guarantee any high level security property. Our research focuses on designing and formally verifying secure low-level platforms. We use a mix of interactive theorem provers and semi-automatic analysis techniques to mathematically prove absence of illicit information flows, integrity of critical resources, and impossibility of execution of untrusted SW. Responsible:

Secure Networks and Systems

We work with topics of mutual interest to the TCS group at KTH Royal Institute of Technology and Ericsson Research. The focus of the cooperation lies on software security, formal verification and cryptography. Responsible:

Practical and Provably Secure Cryptography

We construct, analyze, and implement provably secure cryptographic protocols. Our main application is electronic voting systems. Such protocols are challenging both theoretically and practically due to their heterogeneous structure. The interplay between implementation and theory improves the understanding of both. Responsible: