Ändra sökning
Länk till posten
Permanent länk

Direktlänk
Publikationer (9 of 9) Visa alla publikationer
Baumann, C., Schwarz, O. & Dam, M. (2019). On the verification of system-level information flow properties for virtualized execution platforms. Journal of Cryptographic Engineering, 9(3), 243-261
Öppna denna publikation i ny flik eller fönster >>On the verification of system-level information flow properties for virtualized execution platforms
2019 (Engelska)Ingår i: Journal of Cryptographic Engineering, ISSN 2190-8508, Vol. 9, nr 3, s. 243-261Artikel i tidskrift (Refereegranskat) Published
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.

Ort, förlag, år, upplaga, sidor
Springer Verlag, 2019
Nyckelord
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
Nationell ämneskategori
Naturvetenskap
Identifikatorer
urn:nbn:se:ri:diva-39556 (URN)10.1007/s13389-019-00216-4 (DOI)2-s2.0-85067694646 (Scopus ID)
Tillgänglig från: 2019-07-08 Skapad: 2019-07-08 Senast uppdaterad: 2020-01-30Bibliografiskt granskad
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.
Öppna denna publikation i ny flik eller fönster >>A High Assurance Virtualization Platform for ARMv8
Visa övriga...
2016 (Engelska)Ingår i: 2016 European Conference on Networks and Communications (EuCNC), 2016, 9, s. 210-214, artikel-id 7561034Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Nyckelord
hypervisor, isolation, assurance, formal verification, Common Criteria, ARMv8
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:ri:diva-24570 (URN)10.1109/EuCNC.2016.7561034 (DOI)2-s2.0-84988950416 (Scopus ID)9781509028931 (ISBN)
Konferens
2016 European Conference on Networks and Communications (EUCNC 2016), June 27-30, 2016, Athens, Greece
Projekt
HASPOC
Anmärkning

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.

Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2024-04-11Bibliografiskt granskad
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
Öppna denna publikation i ny flik eller fönster >>Automatic Derivation of Platform Noninterference Properties
2016 (Engelska)Ingår i: Software Engineering and Formal Methods / [ed] Rocco De Nicola, Eva Kühn, 2016, 8, Vol. 9763, s. 27-44Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Serie
Lecture Notes in Computer Science (LNCS), ISSN 0302-9743 ; 9763
Nyckelord
Instruction set architectures, ARM, MIPS, noninterference, information flow, theorem proving, HOL4
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:ri:diva-24556 (URN)10.1007/978-3-319-41591-8_3 (DOI)2-s2.0-84977574405 (Scopus ID)978-3-319-41590-1 (ISBN)978-3-319-41591-8 (ISBN)
Konferens
14th International Conference on Software Engineering and Formal Methods (SEFM 2016), July 4-8, 2016, Vienna, Austria
Projekt
PROSPERHASPOC
Anmärkning

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

Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2020-12-01Bibliografiskt granskad
Blom, R. & Schwarz, O. (2015). High Assurance Security Products on COTS Platforms (7ed.). ERCIM News (102), 39-40
Öppna denna publikation i ny flik eller fönster >>High Assurance Security Products on COTS Platforms
2015 (Engelska)Ingår i: ERCIM News, ISSN 0926-4981, E-ISSN 1564-0094, nr 102, s. 39-40Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
ERCIM EEIG, 2015 Upplaga: 7
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:ri:diva-24462 (URN)
Projekt
HASPOC
Anmärkning

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

Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2024-03-03Bibliografiskt granskad
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).
Öppna denna publikation i ny flik eller fönster >>Affordable Separation on Embedded Platforms: Soft Reboot Enabled Virtualization on a Dual Mode System
2014 (Engelska)Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Nyckelord
Dual Mode Separation Soft Reboot Virtualization Hypervisor Embedded Systems Security
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:ri:diva-24327 (URN)10.1007/978-3-319-08593-7_3 (DOI)2-s2.0-84904168680 (Scopus ID)
Konferens
Trust & Trustworthy Computing (TRUST) 2014
Projekt
PROSPERNSHIELD
Anmärkning

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.

Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2020-12-01Bibliografiskt granskad
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
Öppna denna publikation i ny flik eller fönster >>Formal Verification of Secure User Mode Device Execution with DMA
2014 (Engelska)Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Nyckelord
peripheral devices, DMA, separation, isolation, user mode execution, ARM, formal hardware/software co-verification, theorem proving, HOL4
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:ri:diva-24374 (URN)10.1007/978-3-319-13338-6_18 (DOI)2-s2.0-84921419001 (Scopus ID)9783319133379 (ISBN)
Konferens
Haifa Verification Conference
Projekt
Provably Secure Execution Platforms for Embedded Systems
Anmärkning

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.

Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2020-12-01Bibliografiskt granskad
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).
Öppna denna publikation i ny flik eller fönster >>Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Visa övriga...
2013 (Engelska)Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Nyckelord
Formal verification, Information Flow Security, Separation Kernel, Hypervisor
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:ri:diva-24266 (URN)10.1145/2508859.2516702 (DOI)2-s2.0-84889040001 (Scopus ID)
Konferens
2013 ACM SIGSAC conference on computer & communications security
Projekt
PROSPER
Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2020-12-01Bibliografiskt granskad
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). , Article ID 8307.
Öppna denna publikation i ny flik eller fönster >>Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
2013 (Engelska)Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Nyckelord
ARM instruction set, noninterference, user mode execution, kernel security, theorem proving
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:ri:diva-24275 (URN)10.1007/978-3-319-03545-1_18 (DOI)2-s2.0-84893128835 (Scopus ID)
Konferens
Certified Programs and Proofs (CPP)
Projekt
PROSPER
Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2020-12-01Bibliografiskt granskad
Schwarz, O. & Gehrmann, C. (2012). Securing DMA through Virtualization (20ed.). In: IEEE Conference on Complexity in Engineering: . Paper presented at COMPENG 2012 (pp. 118-123). IEEE, Article ID 6242958.
Öppna denna publikation i ny flik eller fönster >>Securing DMA through Virtualization
2012 (Engelska)Ingår i: IEEE Conference on Complexity in Engineering, IEEE , 2012, 20, s. 118-123, artikel-id 6242958Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
IEEE, 2012 Upplaga: 20
Nyckelord
DMA, virtualization, security, embedded systems, direct memory access, formal verification
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:ri:diva-24036 (URN)10.1109/CompEng.2012.6242958 (DOI)2-s2.0-84866553727 (Scopus ID)978-1-4673-1615-6 (ISBN)978-1-4673-1615-6 (ISBN)
Konferens
COMPENG 2012
Projekt
TNG SecurityPROSPER
Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2021-01-13Bibliografiskt granskad
Organisationer
Identifikatorer
ORCID-id: ORCID iD iconorcid.org/0000-0003-3434-5640

Sök vidare i DiVA

Visa alla publikationer