Assistant professor, Theoretical Computer Science
School of Computer Science and Communication
Reveal my email@example.com
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.
Provably Secure Execution Platforms for Embedded Systems
High Assurance Security Products On COTS platforms
Usable and Efficient Secure Multiparty Computation
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!
- 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.
Some completed thesis and projects:
- 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
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
Roberto Guanciale, Hamed Nemati,
Provably Secure Memory Isolation for Linux on ARM. JCS 2016. To appear
Roberto Guanciale, Emilio Tuosto:
An abstract semantics of the global view of choreographies. ICE 2016: To appear
Roberto Guanciale, Hamed Nemati, Christoph Baumann, Mads Dam:
Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. IEEE Symposium on Security and Privacy 2016: 38-55
Hamed Nemati, Mads Dam, Roberto Guanciale:
Trustworthy Memory Isolation of Linux on
Embedded Devices. TRUST 2015: 125-142
Hind Chfouka, Hamed Nemati, Roberto Guanciale, Mads Dam, Patrik Ekdahl:
Trustworthy Prevention of Code Injection in
Linux on Embedded Devices. ESORICS 2015: 90-107
Dilian Gurov, Peeter Laud, Roberto Guanciale:
Privacy Preserving Business Process Matching. PST 2015: 36-43
Hamed Nemati, Roberto Guanciale, Mads Dam:
Trustworthy Virtualization of the ARMv7 Memory Subsystem. SOFSEM 2015: 578-589
- Roberto Guanciale, Dilian Gurov:
Privacy Preserving Business Process Fusion. BPM Workshops 2014: 96-101
- Musard Balliu, Mads Dam, Roberto Guanciale:
Automating Information Flow Analysis of Low Level Code. ACM Conference on Computer and Communications Security 2014: 1080-1091
- Roberto Guanciale, Dilian Gurov, Peeter Laud:
Private intersection of regular languages. PST 2014: 112-120
Hind Chfouka, Andrea Corradini, Roberto Guanciale: Classification Techniques for Conformance and Performance Checking in Process Analysis. AIBP@AI*IA 2013: 21-30
Mads Dam, Roberto Guanciale, Hamed Nemati: Machine code verification of a tiny ARM hypervisor. TrustED@CCS 2013: 3-12
Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati, Oliver Schwarz: Formal verification of information flow security for a simple arm-based separation kernel. ACM Conference on Computer and Communications Security 2013: 223-234
Roberto Bruni, Andrea Corradini, Gian Luigi Ferrari, Tito Flagella, Roberto Guanciale, Giorgio Spagnolo: Applying Process Analysis to the Italian eGovernment Enterprise Architecture. WS-FM 2011: 111-127
Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto: Model-Driven Development of Long Running Transactions. Results of the SENSORIA Project 2011: 326-348
Laura Bocchi, Roberto Guanciale, Daniele Strollo, Emilio Tuosto: BPMN Modelling of Services with Dynamically Reconfigurable Transactions. ICSOC 2010: 396-410
Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto: Refactoring Long Running Transactions: A Case Study. TGC 2010: 318-334
Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo: Global Coordination Policies for Services. Electr. Notes Theor. Comput. Sci. 260: 73-89 (2010)
Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo: Event based choreography. Sci. Comput. Program. 75(10): 848-878 (2010)
Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto: Event-Based Service Coordination. Concurrency, Graphs and Models 2008: 312-329
Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo: Checking Correctness of Transactional Behaviors. FORTE 2008: 134-148
Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto: Refactoring Long Running Transactions. WS-FM 2008: 127-142
Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto: Debugging Distributed Systems with Causal Nets. ECEASST 14: (2008)
GianLuigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto: Coordination Via Types in an Event-Based Framework. FORTE 2007: 66-80
Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo: JSCL: A Middleware for Service Coordination. FORTE 2006: 46-60
Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo: Event Based Service Coordination over Dynamic and Heterogeneous Networks. ICSOC 2006: 453-458