|
PROSPER
Research LeaderPost Docs and SeniorsGraduate Students
Project Members at SICS Swedish ICTFormer 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 CountermeasuresRoberto 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 Arash Vahidi 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 TrustED 2013. 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 Musard Balliu 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 systemsJonas Haglund M.Sc. thesis. KTH, 2016. No Hypervisor Is an Island: System-wide Isolation Guarantees for Low Level Code Oliver Schwarz PhD thesis, KTH, Trita-CSC-A 2016:22 (ISSN 1653-5723). Logics for Information Flow Security: From Specification to Verification Musard Balliu PhD thesis. KTH, Trita-CSC-A 2014:13 (ISSN 1653-5723). Inlined Reference Monitors: Certification, Concurrency and Tree Based Monitoring Andreas Lundblad PhD thesis. KTH, Trita-CSC-A 2013:01 (ISSN 1653-5723). The Prosper run-time monitor: design and formal verification Hind Chfouka M.Sc. thesis, Pisa University, 2014. A thin MIPS hypervisor for embedded systems Mikael Sahlström M.Sc. thesis, Lund University, 2013. Porting Linux to a Hypervisor Based Embedded System Hariprasad Govindharajan M.Sc. thesis, Uppsala University, 2013. Timevirtualisering för hypervisors Jonas Haglund B.Sc. thesis. KTH, 2012. LinksMain Project Page |
