Change search
Link to record
Permanent link

Direct link
BETA
Publications (10 of 54) Show all publications
Nemati, H., Baumann, C., Guanciale, R. & Dam, M. (2018). Formal verification of integrity-Preserving countermeasures against cache storage side-channels. In: 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018: . Paper presented at 14 April 2018 through 20 April 2018 (pp. 109-133). Springer Verlag
Open this publication in new window or tab >>Formal verification of integrity-Preserving countermeasures against cache storage side-channels
2018 (English)In: 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Springer Verlag , 2018, p. 109-133Conference paper, Published paper (Refereed)
Abstract [en]

Formal verification of systems-level software such as hypervisors and operating systems can enhance system trustworthiness. However, without taking low level features like caches into account the verification may become unsound. While this is a well-known fact w.r.t. timing leaks, few works have addressed latent cache storage side-channels, whose effects are not limited to information leakage. We present a verification methodology to analyse soundness of countermeasures used to neutralise these channels. We apply the proposed methodology to existing countermeasures, showing that they allow to restore integrity of the system. We decompose the proof effort into verification conditions that allow for an easy adaption of our strategy to various software and hardware platforms. As case study, we extend the verification of an existing hypervisor whose integrity can be tampered using cache storage channels. We used the HOL4 theorem prover to validate our security analysis, applying the verification methodology to a generic hardware model. 

Place, publisher, year, edition, pages
Springer Verlag, 2018
Keywords
Cache memory, Hardware, Network security, Hardware models, Information leakage, Low-level features, Security analysis, Software and hardwares, Storage channels, Verification condition, Verification methodology, Formal verification
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:kth:diva-227490 (URN)10.1007/978-3-319-89722-6_5 (DOI)000445805600005 ()2-s2.0-85045658183 (Scopus ID)9783319897219 (ISBN)
Conference
14 April 2018 through 20 April 2018
Note

Conference code: 212909; Export Date: 9 May 2018; Conference Paper; Correspondence Address: Baumann, C.; KTH Royal Institute of TechnologySweden; email: cbaumann@kth.se; Funding details: SSF, Stiftelsen för Strategisk Forskning; Funding details: BMBF, Bundesministerium für Bildung und Forschung; Funding details: 13N1S0762; Funding details: MHE&SR, Ministry of Higher Education and Scientific Research; Funding details: MSB, Myndigheten för Samhällsskydd och Beredskap; Funding text: Acknowledgments. This work was supported by the PROSPER project funded by the Swedish Foundation for Strategic Research, the KTH CERCES Center for Resilient Critical Infrastructures funded by the Swedish Civil Contingencies Agency, as well as the German Federal Ministry of Education and Research (BMBF) through funding for the CISPA-Stanford Center for Cybersecurity (FKZ: 13N1S0762). QC 20180516

QC 20181012

Available from: 2018-05-16 Created: 2018-05-16 Last updated: 2018-10-12Bibliographically approved
Baumann, C., Schwarz, O. & Dam, M. (2017). Compositional Verification of Security Properties for Embedded Execution Platforms. In: Ulrich Kühne and Jean-Luc Danger and Sylvain Guilley (Ed.), PROOFS 2017: 6th International Workshop on Security Proofs for Embedded Systems. Paper presented at PROOFS 2017. 6th International Workshop on Security Proofs for Embedded Systems (pp. 1-16). , 49
Open this publication in new window or tab >>Compositional Verification of Security Properties for Embedded Execution Platforms
2017 (English)In: PROOFS 2017: 6th International Workshop on Security Proofs for Embedded Systems / [ed] Ulrich Kühne and Jean-Luc Danger and Sylvain Guilley, 2017, Vol. 49, p. 1-16Conference paper, Published paper (Refereed)
Abstract [en]

The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system level behaviour, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible. To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage. As a case study, we apply this methodology to the verification of information flow security for an industry scale security-oriented hypervisor on the ARMv8-A platform. The hypervisor statically assigns (multiple) cores to each guest system and implements a rudimentary, but usable, inter guest communication discipline. We have completed a pen-and-paper security proof for the hypervisor down to state transition level and report on a partially completed verification of guest mode security in the HOL4 theorem prover.

Series
EPiC Series in Computing, ISSN 2398-7340
Keywords
ARMv8, hardware platform, formal verification, hypervisor, decomposition, SoC, system security
National Category
Computer Systems Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-215208 (URN)
Conference
PROOFS 2017. 6th International Workshop on Security Proofs for Embedded Systems
Projects
HASPOCPROSPERCERCES
Funder
Swedish Civil Contingencies AgencyVINNOVASwedish Foundation for Strategic Research
Note

QC 20171009

Available from: 2017-10-04 Created: 2017-10-04 Last updated: 2018-01-03Bibliographically approved
Nemati, H., Guanciale, R., Baumann, C. & Dam, M. (2017). Formal Analysis of Countermeasures against Cache Storage Side Channels. Paper presented at -.
Open this publication in new window or tab >>Formal Analysis of Countermeasures against Cache Storage Side Channels
2017 (English)Manuscript (preprint) (Other academic)
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-213405 (URN)
Conference
-
Note

QC 20170830

Available from: 2017-08-30 Created: 2017-08-30 Last updated: 2018-01-13Bibliographically approved
Schwarz, O. & Dam, M. (2016). Automatic Derivation of Platform Noninterference Properties. In: Rocco De Nicola, Eva Kühn (Ed.), Software Engineering and Formal Methods, Springer LNCS 9763: . Paper presented at 14th International Conference on Software Engineering and Formal Methods, SEFM 2016 Held as Part of Conference on Software Technologies: Applications and Foundations, STAF 2016, Vienna, Austria, 4 July 2016 through 8 July 2016 (pp. 27-44). Springer, 9763
Open this publication in new window or tab >>Automatic Derivation of Platform Noninterference Properties
2016 (English)In: Software Engineering and Formal Methods, Springer LNCS 9763 / [ed] Rocco De Nicola, Eva Kühn, Springer, 2016, Vol. 9763, p. 27-44Conference paper, Published paper (Refereed)
Abstract [en]

For the verification of system software, information flow properties of the instruction set architecture (ISA) are essential.They show how information propagates through the processor, including sometimes opaque control registers.Thus, they can be used to guarantee that user processes cannot infer the state of privileged system components, such as secure partitions.Formal ISA models - for example for the HOL4 theorem prover - have been available for a number of years. However, little work has been published on the formal analysis of these models.In this paper, we present a general framework for proving information flow properties of a number of ISAs automatically, for example for ARM.The analysis is represented in HOL4 using a direct semantical embedding of noninterference, and does not use an explicit type system, in order to (i) minimize the trusted computingbase, and to (ii) support a large degree of context-sensitivity, which is needed for the analysis.The framework determines automatically which system components are accessible at a given privilege level, guaranteeing both soundness and accuracy.

Place, publisher, year, edition, pages
Springer, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9763
Keywords
Instruction set architectures, ARM, MIPS, noninterference, information flow, theorem proving, HOL4
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-192451 (URN)10.1007/978-3-319-41591-8_3 (DOI)000386263500003 ()2-s2.0-84977574405 (Scopus ID)978-3-319-41590-1 (ISBN)978-3-319-41591-8 (ISBN)
Conference
14th International Conference on Software Engineering and Formal Methods, SEFM 2016 Held as Part of Conference on Software Technologies: Applications and Foundations, STAF 2016, Vienna, Austria, 4 July 2016 through 8 July 2016
Projects
PROSPERHASPOCCERCES
Funder
VINNOVASwedish Foundation for Strategic Research Swedish Civil Contingencies Agency
Note

QC 20161121

Available from: 2016-09-12 Created: 2016-09-12 Last updated: 2018-01-10Bibliographically approved
Guanciale, R., Nemati, H., Baumann, C. & Dam, M. (2016). Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. In: Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016: . Paper presented at 2016 IEEE Symposium on Security and Privacy, SP 2016, 23 May 2016 through 25 May 2016 (pp. 38-55). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures
2016 (English)In: Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016, Institute of Electrical and Electronics Engineers (IEEE), 2016, p. 38-55Conference paper, Published paper (Refereed)
Abstract [en]

Caches pose a significant challenge to formal proofs of security for code executing on application processors, as the cache access pattern of security-critical services may leak secret information. This paper reveals a novel attack vector, exposing a low-noise cache storage channel that can be exploited by adapting well-known timing channel analysis techniques. The vector can also be used to attack various types of security-critical software such as hypervisors and application security monitors. The attack vector uses virtual aliases with mismatched memory attributes and self-modifying code to misconfigure the memory system, allowing an attacker to place incoherent copies of the same physical address into the caches and observe which addresses are stored in different levels of cache. We design and implement three different attacks using the new vector on trusted services and report on the discovery of an 128-bit key from an AES encryption service running in TrustZone on Raspberry Pi 2. Moreover, we subvert the integrity properties of an ARMv7 hypervisor that was formally verified against a cache-less model. We evaluate well-known countermeasures against the new attack vector and propose a verification methodology that allows to formally prove the effectiveness of defence mechanisms on the binary code of the trusted software.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2016
Keywords
cache storage channels, hypervisor, side channels, verification, Application programs, Codes (symbols), Cryptography, Physical addresses, Side channel attack, Vectors, Virtual addresses, Application processors, Application security, Defence mechanisms, Design and implements, Side-channel, Storage channels, Verification methodology, Cache memory
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:kth:diva-194955 (URN)10.1109/SP.2016.11 (DOI)000387292800003 ()2-s2.0-84987617492 (Scopus ID)9781509008247 (ISBN)
Conference
2016 IEEE Symposium on Security and Privacy, SP 2016, 23 May 2016 through 25 May 2016
Projects
PROSPER, CERCES
Funder
Swedish Foundation for Strategic Research
Note

QC 20161123

Available from: 2016-11-23 Created: 2016-11-01 Last updated: 2017-10-06Bibliographically approved
Buchegger, S. & Dam, M. (Eds.). (2015). Secure IT Systems: 20th Nordic Conference, NordSec 2015 Stockholm, Sweden, October 19-21, 2015 Proceedings. Paper presented at 19 October 2015 through 21 October 2015. Springer
Open this publication in new window or tab >>Secure IT Systems: 20th Nordic Conference, NordSec 2015 Stockholm, Sweden, October 19-21, 2015 Proceedings
2015 (English)Conference proceedings (editor) (Refereed)
Place, publisher, year, edition, pages
Springer, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9417
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-181565 (URN)10.1007/978-3-319-26502-5 (DOI)2-s2.0-84951874651 (Scopus ID)9783319265018 (ISBN)
Conference
19 October 2015 through 21 October 2015
Note

QC 20160229

Available from: 2016-02-03 Created: 2016-02-02 Last updated: 2018-01-10Bibliographically approved
Dam, M., Jacobs, B., Lundblad, A. & Piessens, F. (2015). Security monitor inlining and certification for multithreaded Java. Mathematical Structures in Computer Science, 25(3), 528-565
Open this publication in new window or tab >>Security monitor inlining and certification for multithreaded Java
2015 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 25, no 3, p. 528-565Article in journal (Refereed) Published
Abstract [en]

Security monitor inlining is a technique for security policy enforcement whereby monitor functionality is injected into application code in the style of aspect-oriented programming. The intention is that the injected code enforces compliance with the policy (security), and otherwise interferes with the application as little as possible (conservativity and transparency). Such inliners are said to be correct. For sequential Java-like languages, inlining is well understood, and several provably correct inliners have been proposed. For multithreaded Java one difficulty is the need to maintain a shared monitor state. We show that this problem introduces fundamental limitations in the type of security policies that can be correctly enforced by inlining. A class of race-free policies is identified that precisely characterizes the inlineable policies by showing that inlining of a policy outside this class is either not secure or not transparent, and by exhibiting a concrete inliner for policies inside the class which is secure, conservative and transparent. The inliner is implemented for Java and applied to a number of practical application security policies. Finally, we discuss how certification in the style of proof-carrying code could be supported for inlined programs by using annotations to reduce a potentially complex verification problem for multithreaded Java bytecode to sequential verification of just the inlined code snippets.

Keywords
Aspect oriented programming, Codes (symbols), Computer software, Security systems, Application codes, Application security, Fundamental limitations, Java byte codes, Proof-carrying code, Security monitors, Security policy enforcement, Verification problems
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:kth:diva-62964 (URN)10.1017/S0960129512000916 (DOI)000348369900003 ()2-s2.0-84921923104 (Scopus ID)
Funder
EU, FP7, Seventh Framework Programme
Note

QC 20150303. Updated from submitted to published.

Available from: 2012-01-20 Created: 2012-01-20 Last updated: 2018-01-12Bibliographically approved
Nemati, H., Dam, M., Guanciale, R., Do, V. & Vahidi, A. (2015). Trustworthy Memory Isolation of Linux on Embedded Devices. In: Trust and Trustworthy Computing, TRUST 2015: . Paper presented at 8th International Conference on Trust and Trustworthy Computing (TRUST), AUG 24-26, 2015, Fdn Res & Technol Hellas, Inst Comp Sci, Heraklion, GREECE (pp. 125-142). Springer Berlin/Heidelberg
Open this publication in new window or tab >>Trustworthy Memory Isolation of Linux on Embedded Devices
Show others...
2015 (English)In: Trust and Trustworthy Computing, TRUST 2015, Springer Berlin/Heidelberg, 2015, p. 125-142Conference paper, Published paper (Refereed)
Abstract [en]

The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself, for instance by run-time monitoring. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a virtualization platform for the ARMv7-A processor family. Our design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen for the x86 architecture, and used later with minor variants by the Secure Virtual Architecture, SVA. We show that the direct paging mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the ARMv7-A ISA, including the MMU. We prove memory isolation of the hosted components along with information flow security for an abstract top level model of the virtualization mechanism. The abstract model is refined down to a HOL4 transition system closely resembling a C implementation. The virtualization mechanism is demonstrated on real hardware via a hypervisor capable of hosting Linux as an untrusted guest.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9229
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-177437 (URN)10.1007/978-3-319-22846-4_8 (DOI)000363795400008 ()2-s2.0-84944529938 (Scopus ID)978-3-319-22846-4 (ISBN)978-3-319-22845-7 (ISBN)
Conference
8th International Conference on Trust and Trustworthy Computing (TRUST), AUG 24-26, 2015, Fdn Res & Technol Hellas, Inst Comp Sci, Heraklion, GREECE
Funder
Swedish Foundation for Strategic Research
Note

QC 20160714

Available from: 2015-11-20 Created: 2015-11-20 Last updated: 2018-01-10Bibliographically approved
Chfouka, H., Nemati, H., Guanciale, R., Dam, M. & Ekdahl, P. (2015). Trustworthy prevention of code injection in Linux on embedded devices. In: 20th European Symposium on Research in Computer Security, ESORICS 2015: . Paper presented at 20th European Symposium on Research in Computer Security, ESORICS 2015; Vienna; Austria (pp. 90-107). Springer
Open this publication in new window or tab >>Trustworthy prevention of code injection in Linux on embedded devices
Show others...
2015 (English)In: 20th European Symposium on Research in Computer Security, ESORICS 2015, Springer, 2015, p. 90-107Conference paper, Published paper (Refereed)
Abstract [en]

We present MProsper, a trustworthy system to prevent code injection in Linux on embedded devices. MProsper is a formally verified run-time monitor, which forces an untrusted Linux to obey the executable space protection policy; a memory area can be either executable or writable, but cannot be both. The executable space protection allows the MProsper’s monitor to intercept every change to the executable code performed by a user application or by the Linux kernel. On top of this infrastructure, we use standard code signing to prevent code injection. MProsper is deployed on top of the Prosper hypervisor and is implemented as an isolated guest. Thus MProsper inherits the security property verified for the hypervisor: (i) Its code and data cannot be tampered by the untrusted Linux guest and (ii) all changes to the memory layout is intercepted, thus enabling MProsper to completely mediate every operation that can violate the desired security property. The verification of the monitor has been performed using the HOL4 theorem prover and by extending the existing formal model of the hypervisor with the formal specification of the high level model of the monitor.

Place, publisher, year, edition, pages
Springer, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9326
Keywords
Codes (symbols), Embedded systems, Linux, Security of data, Security systems, Systems analysis, Embedded device, Executable codes, High-level modeling, Protection policy, Security properties, Standard codes, Theorem provers, Trustworthy systems, Computer operating systems
National Category
Computer Systems
Identifiers
urn:nbn:se:kth:diva-181591 (URN)10.1007/978-3-319-24174-6_5 (DOI)000374478000005 ()2-s2.0-84951274986 (Scopus ID)9783319241739 (ISBN)
Conference
20th European Symposium on Research in Computer Security, ESORICS 2015; Vienna; Austria
Funder
Swedish Foundation for Strategic Research
Note

QC 20160204

Available from: 2016-02-04 Created: 2016-02-02 Last updated: 2017-08-28Bibliographically approved
Nemati, H., Guanciale, R. & Dam, M. (2015). Trustworthy virtualization of the ARMv7 memory subsystem. In: 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015: . Paper presented at 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015; Pec pod Sněžkou; Czech Republic; 24 January 2015 through 29 January 2015 (pp. 578-589). Springer Berlin/Heidelberg
Open this publication in new window or tab >>Trustworthy virtualization of the ARMv7 memory subsystem
2015 (English)In: 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015, Springer Berlin/Heidelberg, 2015, p. 578-589Conference paper, Published paper (Refereed)
Abstract [en]

In order to host a general purpose operating system, hypervisors need to virtualize the CPU memory subsystem. This entails dynamically changing MMU resources, in particular the page tables, to allow a hosted OS to reconfigure its own memory. In this paper we present the verification of the isolation properties of a hypervisor design that uses direct paging. This virtualization approach allows to host commodity Oss without requiring either shadow data structures or specialized hardware support. Our verification targets a system consisting of a commodity CPU for embedded devices (ARMv7), a hypervisor and an untrusted guest running Linux.The verification involves three steps: (i) Formalization of an ARMv7 CPU that includes the MMU, (ii) Formalization of a system behavior that includes the hypervisor and the untrusted guest (iii) Verification of the isolation properties. Formalization and proof are done in the HOL4 theorem prover, thus allowing to re-use the existing HOL4 ARMv7 model developed in Cambridge.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8939
Keywords
Formal verification, Hypervisor, Memory management, Theorem proving, Virtual reality, Embedded device, Memory subsystems, Specialized hardware, System behaviors, Theorem provers, Virtualizations, Memory management units
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:kth:diva-167389 (URN)10.1007/978-3-662-46078-8_48 (DOI)000357679300047 ()2-s2.0-84922031791 (Scopus ID)9783662460771 (ISBN)
Conference
41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015; Pec pod Sněžkou; Czech Republic; 24 January 2015 through 29 January 2015
Note

QC 20150529

Available from: 2015-05-29 Created: 2015-05-22 Last updated: 2018-01-11Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0001-5432-6442

Search in DiVA

Show all publications