Change search
Link to record
Permanent link

Direct link
BETA
Publications (9 of 9) Show all publications
Baumann, C., Schwarz, O. & Dam, M. (2019). On the verification of system-level information flow properties for virtualized execution platforms. Journal of Cryptographic Engineering
Open this publication in new window or tab >>On the verification of system-level information flow properties for virtualized execution platforms
2019 (English)In: Journal of Cryptographic Engineering, ISSN 2190-8508Article in journal (Refereed) Epub ahead of print
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 behavior, 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 and report on the complete verification of guest mode security properties in the HOL4 theorem prover.

Place, publisher, year, edition, pages
Springer Verlag, 2019
Keywords
ARMv8, Decomposition, Formal verification, Hypervisor, Information flow security, SoC, ARM processors, Embedded systems, Message passing, Network security, Programmable logic controllers, Specifications, System-on-chip, Abstract specifications, Embedded system specifications, Execution platforms, Security properties, Top down approaches
National Category
Natural Sciences
Identifiers
urn:nbn:se:ri:diva-39556 (URN)10.1007/s13389-019-00216-4 (DOI)2-s2.0-85067694646 (Scopus ID)
Available from: 2019-07-08 Created: 2019-07-08 Last updated: 2019-07-08Bibliographically approved
Baumann, C., Näslund, M., Gehrmann, C., Schwarz, O. & Thorsen, H. (2016). A High Assurance Virtualization Platform for ARMv8 (9ed.). In: 2016 European Conference on Networks and Communications (EuCNC): . Paper presented at 2016 European Conference on Networks and Communications (EUCNC 2016), June 27-30, 2016, Athens, Greece (pp. 210-214). , Article ID 7561034.
Open this publication in new window or tab >>A High Assurance Virtualization Platform for ARMv8
Show others...
2016 (English)In: 2016 European Conference on Networks and Communications (EuCNC), 2016, 9, p. 210-214, article id 7561034Conference paper, Published paper (Refereed)
Abstract [en]

This paper presents the first results from the ongoing research project HASPOC, developing a high assurance virtualization platform for the ARMv8 CPU architecture. Formal verification at machine code level guarantees information isolation between different guest systems (e.g.~OSs) running on the platform. To use the platform in networking scenarios, we allow guest systems to securely communicate with each other via platform-provided communication channels and to take exclusive control of peripherals for communication with the outside world. The isolation is shown to be formally equivalent to that of guests executing on physically separate platforms with dedicated communication channels crossing the air-gap. Common Criteria (CC) assurance methodology is applied by preparing the CC documentation required for an EAL6 evaluation of products using the platform. Besides the hypervisor, a secure boot component is included and verified to ensure system integrity.

Keywords
hypervisor, isolation, assurance, formal verification, Common Criteria, ARMv8
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:ri:diva-24570 (URN)10.1109/EuCNC.2016.7561034 (DOI)9781509028931 (ISBN)
Conference
2016 European Conference on Networks and Communications (EUCNC 2016), June 27-30, 2016, Athens, Greece
Projects
HASPOC
Note

This is the author version of the corresponding paper published in the 2016 European Conference on Networks and Communications (EuCNC). The publisher is IEEE. The final publication (DOI: 10.1109/EuCNC.2016.7561034) is available at IEEE Xplore via http://ieeexplore.ieee.org/document/7561034 © © 2016 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2019-06-12Bibliographically approved
Schwarz, O. & Dam, M. (2016). Automatic Derivation of Platform Noninterference Properties (8ed.). In: Rocco De Nicola, Eva Kühn (Ed.), Software Engineering and Formal Methods: . Paper presented at 14th International Conference on Software Engineering and Formal Methods (SEFM 2016), July 4-8, 2016, Vienna, Austria (pp. 27-44). , 9763
Open this publication in new window or tab >>Automatic Derivation of Platform Noninterference Properties
2016 (English)In: Software Engineering and Formal Methods / [ed] Rocco De Nicola, Eva Kühn, 2016, 8, 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 computing base, 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.

Series
Lecture Notes in Computer Science (LNCS), ISSN 0302-9743 ; 9763
Keywords
Instruction set architectures, ARM, MIPS, noninterference, information flow, theorem proving, HOL4
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:ri:diva-24556 (URN)10.1007/978-3-319-41591-8_3 (DOI)978-3-319-41590-1 (ISBN)978-3-319-41591-8 (ISBN)
Conference
14th International Conference on Software Engineering and Formal Methods (SEFM 2016), July 4-8, 2016, Vienna, Austria
Projects
PROSPERHASPOC
Note

This is the author version of the correspondent paper published in "Software Engineering and Formal Methods", the proceedings of SEFM 2016 (editors: Rocco De Nicola, Eva Kühn), Springer LNCS 9763. The publisher is Springer International Publishing Switzerland. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-41591-8_3

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2019-07-10Bibliographically approved
Blom, R. & Schwarz, O. (2015). High Assurance Security Products on COTS Platforms (7ed.). ERCIM News (102), 39-40
Open this publication in new window or tab >>High Assurance Security Products on COTS Platforms
2015 (English)In: ERCIM News, ISSN 0926-4981, E-ISSN 1564-0094, no 102, p. 39-40Article in journal (Refereed) Published
Abstract [en]

With commodity operating systems failing to establish unbreakable isolation of processes, there is a need for stronger separation mechanisms. A recently launched open source project aims at applying virtualization to achieve such isolation on the widespread embedded ARM architectures. Strong assurance is established by formal verification and common criteria certification. Coexisting guest systems are able to run unmodified on the multicore platform, in a resource and cost efficient manner. The solution is rounded anchored in a secure boot process.

Place, publisher, year, edition, pages
ERCIM EEIG, 2015 Edition: 7
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:ri:diva-24462 (URN)
Projects
HASPOC
Note

This is the author version. The publisher's version can be found at http://ercim-news.ercim.eu/en102/r-i/high-assurance-security-products-on-cots-platforms

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2019-07-05Bibliographically approved
Schwarz, O., Gehrmann, C. & Do, V. (2014). Affordable Separation on Embedded Platforms: Soft Reboot Enabled Virtualization on a Dual Mode System (8ed.). In: : . Paper presented at Trust & Trustworthy Computing (TRUST) 2014 (pp. 37-54).
Open this publication in new window or tab >>Affordable Separation on Embedded Platforms: Soft Reboot Enabled Virtualization on a Dual Mode System
2014 (English)Conference paper, Published paper (Refereed)
Abstract [en]

While security has become important in embedded systems, commodity operating systems often fail in effectively separating processes, mainly due to a too large trusted computing base. System virtualization can establish isolation already with a small code base, but many existing embedded CPU architectures have very limited virtualization hardware support, so that the performance impact is often non-negligible. Targeting both security and performance, we investigate an approach in which a few minor hardware additions together with virtualization offer protected execution in embedded systems while still allowing non-virtualized execution when secure services are not needed. Benchmarks of a prototype implementation on an emulated ARM Cortex A8 platform confirm that switching between those two execution forms can be done efficiently.

Keywords
Dual Mode Separation Soft Reboot Virtualization Hypervisor Embedded Systems Security
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:ri:diva-24327 (URN)10.1007/978-3-319-08593-7_3 (DOI)2-s2.0-84904168680 (Scopus ID)
Conference
Trust & Trustworthy Computing (TRUST) 2014
Projects
PROSPERNSHIELD
Note

This is the author version of the correspondent paper published in the proceedings of TRUST 2014 (editors: Thorsten Holz, Sotiris Ioannidis), Springer LNCS 8564. The publisher is Springer International Publishing Switzerland. The final publication is available at http://link.springer.com/10.1007/978-3-319-08593-7_3.

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2019-08-08Bibliographically approved
Schwarz, O. & Dam, M. (2014). Formal Verification of Secure User Mode Device Execution with DMA (9ed.). In: : . Paper presented at Haifa Verification Conference (pp. 236-251). , 8855
Open this publication in new window or tab >>Formal Verification of Secure User Mode Device Execution with DMA
2014 (English)Conference paper, Published paper (Refereed)
Abstract [en]

Separation between processes on top of an operating system or between guests in a virtualized environment is essential for establishing security on modern platforms. A key requirement of the underlying hardware is the ability to support multiple partitions executing on the shared hardware without undue interference. For modern processor architectures - with hardware support for memory management, several modes of operation and I/O interfaces - this is a delicate issue requiring deep analysis at both instruction set and processor implementation level. In a first attempt to rigorously answer this type of questions we introduced in previous work an information flow analysis of user program execution on an ARMv7 platform with hardware supported memory protection, but without I/O. The analysis was performed as a semi-automatic proof search procedure on top of an ARMv7 ISA model implemented in the Cambridge HOL4 theorem prover by Fox et al. The restricted platform functionality, however, makes the analysis of limited practical value. In this paper we add support for devices, including DMA, to the analysis. To this end, we propose an approach to device modeling based on the idea of executing devices nondeterministically in parallel with the (single-core) deterministic processor, covering a fine granularity of interactions between the model components. Based on this model and taking the ARMv7 ISA as an example, we provide HOL4 proofs of several noninterference-oriented isolation properties for a partition executing in the presence of devices which potentially use DMA or interrupts.

Keywords
peripheral devices, DMA, separation, isolation, user mode execution, ARM, formal hardware/software co-verification, theorem proving, HOL4
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:ri:diva-24374 (URN)10.1007/978-3-319-13338-6_18 (DOI)2-s2.0-84921419001 (Scopus ID)9783319133379 (ISBN)
Conference
Haifa Verification Conference
Projects
Provably Secure Execution Platforms for Embedded Systems
Note

This is the author version of the correspondent paper published in “Hardware and Software: Verification and Testing”, the proceedings of HVC 2014 (editor: Eran Yahav), Springer LNCS 8855. The publisher is Springer International Publishing Switzerland. The final publication is available at http://link.springer.com/10.1007/978-3-319-13338-6_18.

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2019-08-09Bibliographically approved
Dam, M., Guanciale, R., Khakpour, N., Nemati, H. & Schwarz, O. (2013). Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel (10ed.). In: : . Paper presented at 2013 ACM SIGSAC conference on computer & communications security (pp. 223-234).
Open this publication in new window or tab >>Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Show others...
2013 (English)Conference paper, Published paper (Refereed)
Abstract [en]

A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a simple separation kernel for ARMv7. Previous work on information flow kernel security leaves communication to be handled by model-external means, and cannot be used to draw conclusions when there is explicit interaction between partitions. We propose a different approach where communication between partitions is made explicit and the information flow is analyzed in the presence of such a channel. Limiting the kernel functionality as much as meaning-fully possible, we accomplish a detailed analysis and verification of the system, proving its correctness at the level of the ARMv7 assembly. As a sanity check we show how the security condition is reduced to noninterference in the special case where no communication takes place. The verification is done in HOL4 taking the Cambridge model of ARM as basis, transferring verification tasks on the actual assembly code to an adaptation of the BAP binary analysis tool developed at CMU.

Keywords
Formal verification, Information Flow Security, Separation Kernel, Hypervisor
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:ri:diva-24266 (URN)10.1145/2508859.2516702 (DOI)
Conference
2013 ACM SIGSAC conference on computer & communications security
Projects
PROSPER
Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2018-08-15Bibliographically approved
Khakpour, N., Schwarz, O. & Dam, M. (2013). Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties (9ed.). In: : . Paper presented at Certified Programs and Proofs (CPP) (pp. 276-291).
Open this publication in new window or tab >>Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
2013 (English)Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we formally verify security properties of the ARMv7 Instruction Set Architecture (ISA) for user mode executions. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. This work establishes a main requirement for operating system and hypervisor verification, as demonstrated for the PROSPER separation kernel. The proof is performed in the HOL4 theorem prover, taking the Cambridge model of ARM as basis. To this end, a proof tool has been developed, which assists the verification of relational state predicates semi-automatically.

Keywords
ARM instruction set, noninterference, user mode execution, kernel security, theorem proving
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:ri:diva-24275 (URN)
Conference
Certified Programs and Proofs (CPP)
Projects
PROSPER
Note

This is the author version of the correspondent paper published in the proceedings of Certified Programs and Proofs 2013 (CPP; editors: G. Gonthier and M. Norrish), Springer LNCS 8307. The publisher is Springer International Publishing Switzerland . The final publication is available at http://link.springer.com/10.1007/978-3-319-03545-1_18.

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2018-08-15Bibliographically approved
Schwarz, O. & Gehrmann, C. (2012). Securing DMA through Virtualization (20ed.). In: IEEE Conference on Complexity in Engineering: . Paper presented at COMPENG 2012. IEEE
Open this publication in new window or tab >>Securing DMA through Virtualization
2012 (English)In: IEEE Conference on Complexity in Engineering, IEEE , 2012, 20Conference paper, Published paper (Refereed)
Abstract [en]

We present a solution for preventing guests in a virtualized system from using direct memory access (DMA) to access memory regions of other guests. The principles we suggest, and that we also have implemented, are purely based on software and standard hardware. No additional virtualization hardware such as an I/O Memory Management Unit (IOMMU) is needed. Instead, the protection of the DMA controller is realized with means of a common ARM MMU only. Overhead occurs only in pre- and postprocessing of DMA transfers and is limited to a few microseconds. The solution was designed with focus on security and the abstract concept of the approach was formally verified.

Place, publisher, year, edition, pages
IEEE, 2012 Edition: 20
Keywords
DMA, virtualization, security, embedded systems, direct memory access, formal verification
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:ri:diva-24036 (URN)10.1109/CompEng.2012.6242958 (DOI)978-1-4673-1615-6 (ISBN)978-1-4673-1615-6 (ISBN)
Conference
COMPENG 2012
Projects
TNG SecurityPROSPER
Note

ISBN: 978-1-4673-1614-9. Copyright 2012 IEEE. Published in the Proceedings of the 2nd IEEE International Conference on Complexity in Engineering, June 11-13, 2012, Aachen, Germany. DOI: 10.1109/CompEng.2012.6242958. Obtainable from http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6242958. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works.

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2018-08-16Bibliographically approved
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0003-3434-5640

Search in DiVA

Show all publications
v. 2.35.7