Post Docs and Seniors
Project Members at SICS Swedish ICT
Former Project Members
Short DescriptionPROSPER (Provably Secure Execution Platforms for Embedded Systems) aims to build the next generation framework for fully verified, secure hypervisors for embedded systems. The following components constitute the core of the project:
FundingThe project is funded by SSF.
Conference PublicationsCache Storage Channels: Alias-Driven Attacks and Verified Countermeasures
Roberto Guanciale, Hamed Nemati, Christoph Baumann, and Mads Dam
37th IEEE Symposium on Security and Privacy, 2016.
Automatic Derivation of Platform Noninterference Properties
Oliver Schwarz and Mads Dam
Software Engineering and Formal Methods (SEFM) 2016.
A high assurance virtualization platform for ARMv8
Christoph Baumann, Mats Näslund, Christian Gehrmann, Oliver Schwarz, and Hans Thorsen
European Conference on Networks and Communications (EuCNC) 2016.
Trustworthy Prevention of Code Injection in Linux on Embedded Devices
Hind Chfouka, Hamed Nemati, Roberto Guanciale, Mads Dam, and Patrik Ekdahl
European Symposium on Research in Computer Security (ESORICS), September 2015.
Trustworthy Memory Isolation of Linux on Embedded Devices
Hamed Nemati, Mads Dam, Roberto Guanciale, Viktor Do and Arash Vahidi
Trust and Trustworthy Computing (TRUST), August 2015.
Security Monitor Inlining and Certification for Multithreaded Java
Mads Dam, Bart Jacobs, Andreas Lundblad, and Frank Piessens
Journal of Mathematical Structures in Computer Science, Volume 25, Number 3, March 2015.
Trustworthy Virtualization of the ARMv7 Memory Subsystem
Hamed Nemati, Roberto Guanciale, and Mads Dam
SOFSEM 2015: Theory and Practice of Computer Science, January 2015.
Formal Verification of Secure User Mode Device Execution with DMA
Oliver Schwarz and Mads Dam
Hardware and Software: Verification and Testing. Haifa Verification Conference (HVC) 2014.
Automating Information Flow Analysis of Low Level Code
Musard Balliu, Mads Dam and Roberto Guanciale
Proceedings of the 21st ACM Conference on Computer and Communication Security (CCS'14) , Scottsdale, Arizona, USA, November 2014.
The Monotonic Separation Kernel
12th IEEE International Conference on Embedded and Ubiquitous Computing, Milan, Italy, 26-28 August, 2014.
Affordable Separation on Embedded Platforms: Soft Reboot Enabled Virtualization on a Dual Mode System
Oliver Schwarz, Christian Gehrmann and Viktor Do
Proceedings of Trust and Trustworthy Computing (TRUST) 2014.
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
Narges Khakpour, Oliver Schwarz and Mads Dam
Certified Programs and Proofs (CPP) 2013.
Machine Code Verification of a Tiny ARM Hypervisor
Mads Dam, Roberto Guanciale and Hamed Nemati
Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati and Oliver Schwarz
Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13).
A Logic for Information Flow Analysis of Distributed Programs
18th Nordic Conference on Secure IT Systems, NordSec 2013, Ilulissat, Greenland, October 18-21, 2013.
(also available as extended version)
Secure RPC in Embedded Systems - Evaluation of some Global Platform Implementation Alternatives
Arash Vahidi and Christopher Jämthagen
8th Workshop on Embedded Systems Security (WESS 2013).
TreeDroid: A Tree Automaton Based Approach to Enforcing Data Processing Policies
Mads Dam, Gurvan Le Guernic, Andreas Lundblad
Proceedings of the 2012 ACM SIGSAC Conference on Computer & Communications Security (CCS'12).
ENCOVER: Symbolic Exploration for Information Flow Security
Musard Balliu, Mads Dam and Gurvan Le Guernic
Proceedings of the IEEE Computer Security Foundations Symposium (CSF '12 ). Harvard University, Cambridge MA, June 25-27, 2012.
Securing DMA through Virtualization
Oliver Schwarz and Christian Gehrmann
2012 IEEE Workshop on Complexity in Engineering (COMPENG 2012), 11-13 June 2012, Aachen, Germany.
ThesesFormal verification of systems software: No execution of malicious software in Linux in networked embedded systems
M.Sc. thesis. KTH, 2016.
No Hypervisor Is an Island: System-wide Isolation Guarantees for Low Level Code
PhD thesis, KTH, Trita-CSC-A 2016:22 (ISSN 1653-5723).
Logics for Information Flow Security: From Specification to Verification
PhD thesis. KTH, Trita-CSC-A 2014:13 (ISSN 1653-5723).
Inlined Reference Monitors: Certification, Concurrency and Tree Based Monitoring
PhD thesis. KTH, Trita-CSC-A 2013:01 (ISSN 1653-5723).
The Prosper run-time monitor: design and formal verification
M.Sc. thesis, Pisa University, 2014.
A thin MIPS hypervisor for embedded systems
M.Sc. thesis, Lund University, 2013.
Porting Linux to a Hypervisor Based Embedded System
M.Sc. thesis, Uppsala University, 2013.
Timevirtualisering för hypervisors
B.Sc. thesis. KTH, 2012.
LinksMain Project Page