Roberto Guanciale

Assistant professor, Theoretical Computer Science
School of Computer Science and Communication

Reveal my mail@kth.se

Lindstedtsvägen 3, Building D, level 5, room 4525
SE-100 44 Stockholm, Sweden

My research interests include formal modeling and verification of systems. I'm currently involved in verification of machine code and application of secure multiparty computation.

Research Projects

Trustfull: Trustworthy Fullstack Computing[Trustfull]

Provably Secure Execution Platforms for Embedded Systems [PROSPER]

High Assurance Security Products On COTS platforms [HASPOC]

Usable and Efficient Secure Multiparty Computation [UaESMC]

Students, get involved!

We encourage students to get involved in our research projects, be it on a hobby basis, as course work, student project, thesis project, student jobs ... You name it!
Some proposals:

• Verification of hardware peripherals: In order to make a computer useful, operating systems and system software must interact with several external peripherals, ranging from input/output devices (e.g. UART, USB, network controllers) and interrupt controllers to coprocessors (e.g. GPU, FPGA). Recently formal techniques have been used to achieve a detailed verification of system software, making it possible to provide low-level platforms with unprecedented security guarantees. However, the interactions among this software and the external peripherals are usually not part of the verification. The external peripherals are assumed to satisfy a set of functional invariants; if these assumptions are not met, an attacker may potentially abuse these components to compromise the entire system. The goal of this project is to model the behavior of real HW peripherals and develop techniques (using bounded model checking) to check if these assumptions are respected by the external peripherals, thus allowing to reconcile trust in the system software.
• Formal verified AES implementation Encryption is one of the key pillars of secure distributed systems. As famous incidents demonstrate (e.g. Heartbleed), using well-tested and certified encryption algorithms is not enough to guarantee security: the software implementation can be buggy, leading to unexpected information leakage, or it can be target of side channel attacks (e.g. by measuring data movement between CPU and memory of the hardware running the implementation, or by observing variations in how long it takes to perform cryptographic operations). To ensure trustworthy encryption, software implementations should be proved to be bug free, possibly extending this verification to cover the actual binary code executed by the CPU. This permits to disregard correctness of the used compiler, which can contain bugs or be compromised (e.g. Xcode Ghost silently infected applications by inserting malicious code at compile time). The aim of this project is to formally verify the binary code of an AES implementation for embedded devices and demonstrate that it is secure: free of bugs, free of memory overflows, and that does not leak information via well known side channels. The project will make use of the HOL4 theorem prover and detailed formal models of ARM CPUs. The verification process involves analyzing the binary code of the AES implementation, this will make the results not depending on correctness of the compiler. Another task consists in experimenting with variations of the original AES code in order to implement different countermeasures against side channel attacks.
• Trustworthy platform for binary analysis The vision of perfect hack-proof code does not seem anymore an utopia. Recently formal techniques have been used to achieve detailed verification of real software, making it possible to provide low-level platforms with unprecedented security guarantees. For such system software, limiting the verification to the source code level is undesirable. A modern compiler consists of several millions of line of code (in contrast to a few thousand lines of code of a microkernel), making it difficult to trust its output even when optimizations are disabled. Recently, Xcode Ghost silently infected applications by inserting malicious code at compile time, compromising the devices of millions of users. The need of semi-automatic analysis techniques for binary code lead to the introduction of several platforms, which provide tools to compute and analyze control-flow graphs, to per- form abstract interpretation and symbolic execution, to verify contracts (via generation of weakest preconditions), and to enforce information flow properties (e.g. via relational analysis). These platforms share a common design; the introduction of hardware independent intermediate representations. The usage of these platforms in a verification exercise is appealing due to the high degree of automation they provide, but it introduces the need of trusting both the correctness of the analysis and the soundness of the translation of machine code in the intermediary language. During the last year, our group focused on guaranteeing soundness of the translation. We formally modeled one of these intermediary languages (the one of the Binary Analysis Platform) in the interactive HOL4 theorem prover and we implemented a proof producing transpiler. This tool translates ARMv8 programs to the intermediary language and generates a HOL4 proof that demonstrates its correctness. The aim of this project is to guarantee correctness of the analysis by re-implementing existing analysis techniques (or possibly new ones) in the Interactive Theorem Prover, so that the resulting tool can generates a proof demonstrating that the conducted analyses are error free. Project will focus on contract based analyses. A common verification task requires to check that, assuming the precondition P is met by the initial state, the execution of the program C produces a state satisfying the postcondition Q. A semi-automatic mechanism to perform this task consists in (1) analyzing the program C and using an algorithm to generate the “weakest precondition” WP that must be satisfied by the initial state to ensure that Q is established, and (2) check that the precondition P entails the weakest precondition WP. During the project an algorithm to generate the weakest preconditions of BAP programs will be implemented in HOL4. The implementation will use HOL4 to generate proofs that justify the correctness of the algorithm’s output.

• Formal verification of a run-time monitor to prevent code-injection in Linux
• Secure isulation of a newtork interface controller
• Rasperry-pi2 port of the Prosper hypervisor
• Multicore extensions of the Prosper hypervisor

Education

2009 IMT Institute for Advanced Studies Lucca: Phd in Computer Science

2004 University of Pisa: Master, Computer Science

2003 University of Pisa: Bachelor, Computer Science

Publications