kth.sePublications
Change search
Link to record
Permanent link

Direct link
Publications (10 of 67) Show all publications
Dong, N., Guanciale, R., Dam, M. & Lööw, A. (2023). Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. In: Alexander Nadel; Kristin Yvonne Rozier (Ed.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023: . Paper presented at Formal Methods in Computer-Aided Design (FMCAD) 2023, 24-27 Oct. 2023. TU Wien Academic Press
Open this publication in new window or tab >>Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor
2023 (English)In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 / [ed] Alexander Nadel; Kristin Yvonne Rozier, TU Wien Academic Press , 2023Conference paper, Published paper (Refereed)
Abstract [en]

We present an in-order pipelined processor and its verification in the HOL4 interactive theorem prover. The processor implements the RISC ISA Silver and features a general 5-stage pipeline. The correctness of the processor is proved by exhibiting a refinement relation between the traces of the pipelined circuit and the Silver ISA. The processor is constructed by using a HOL4 Verilog library for formally verified hardware, and its correctness is guaranteed down to the Verilog implementation. Additionally, we analyze the information flow properties of the processor by utilizing the refinement relation. The notion of conditional noninterference formulates that a processor should not leak more information via its timing channel than what is expected by a leakage model expressed at the ISA level. We establish the conditional noninterference for our processor and demonstrate the adaptability of the information flow methodology to accommodate various processor designs, attacker models, and environments. Our approach to verify processor implementations and enable information flow analysis at the circuit level is suitable for ISAs beyond Silver.

Place, publisher, year, edition, pages
TU Wien Academic Press, 2023
Keywords
Formal Verification, Information Flow, Pipelined Processor, Interactive Theorem Prover
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-338911 (URN)10.34727/2023/isbn.978-3-85448-060-0_33 (DOI)2-s2.0-85180375645 (Scopus ID)
Conference
Formal Methods in Computer-Aided Design (FMCAD) 2023, 24-27 Oct. 2023
Funder
Swedish Foundation for Strategic Research
Note

QC 20231121

Available from: 2023-11-21 Created: 2023-11-21 Last updated: 2024-01-04Bibliographically approved
Guanciale, R., Baumann, C., Buiras, P., Dam, M. & Nemati, H. (2022). A Case Study in Information Flow Refinement for Low Level Systems. In: The Logic of Software. A Tasting Menu of Formal Methods: (pp. 54-79). Springer Nature
Open this publication in new window or tab >>A Case Study in Information Flow Refinement for Low Level Systems
Show others...
2022 (English)In: The Logic of Software. A Tasting Menu of Formal Methods, Springer Nature , 2022, p. 54-79Chapter in book (Other academic)
Abstract [en]

In this work we employ information-flow-aware refinement to study security properties of a separation kernel. We focus on refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We leverage an epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system’s permitted information flows that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. In particular, we show that a simple key manager may cause information leakage via a refinement that includes cache and timing information. Finally, we show that deploying standard countermeasures against cache-based timing channels regains ignorance preservation.

Place, publisher, year, edition, pages
Springer Nature, 2022
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 13360
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-318002 (URN)10.1007/978-3-031-08166-8_4 (DOI)2-s2.0-85133695692 (Scopus ID)
Note

QC 20220916

Available from: 2022-09-16 Created: 2022-09-16 Last updated: 2022-09-16Bibliographically approved
Palmskog, K., Yao, X., Dong, N., Guanciale, R. & Dam, M. (2022). Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022: . Paper presented at 2022 Formal Methods in Computer-Aided Design (FMCAD), 17-21 October 2022, Trento, Italy (pp. 129-138). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Show others...
2022 (English)In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, Institute of Electrical and Electronics Engineers (IEEE) , 2022, p. 129-138Conference paper, Published paper (Refereed)
Abstract [en]

Program analyses based on Instruction Set Architecture (ISA) abstractions can be circumvented using microarchitectural vulnerabilities, permitting unwanted program information flows even when proven ISA-level properties ostensibly rule them out. However, the low abstraction levels found below ISAs, e.g., in microarchitectures defined in hardware description languages, may obscure information flow and hinder analysis tool development. We present a machine-checked formalization in the HOL4 theorem prover of a language, MIL, that abstractly describes microarchitectural in-order and out-of-order program execution and enables reasoning about low-level program information flows. In particular, MIL programs can exhibit information flow side channels when executed out-of-order, as compared to a reference in-order execution. We prove memory consistency between MIL's out-of-order and in-order dynamic semantics in HOL4, and define a notion of conditional noninterference for MIL programs which rules out trace-driven cache side channels. We then demonstrate how to establish conditional noninterference for programs via a novel semi-automated bisimulation based verification strategy inside HOL4 that we apply to several examples. Based on our results, we believe MIL is suitable as a translation target for ISA code to enable information flow analyses.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2022
Series
Formal Methods in Computer-Aided Design
Keywords
HOL4, information flow, interactive theorem proving, microarchitectures, out-of-order execution
National Category
Computer Systems
Identifiers
urn:nbn:se:kth:diva-330691 (URN)10.34727/2022/isbn.978-3-85448-053-2_19 (DOI)001062691400019 ()2-s2.0-85148099314 (Scopus ID)
Conference
2022 Formal Methods in Computer-Aided Design (FMCAD), 17-21 October 2022, Trento, Italy
Note

Part of ISBN 9783854480532

QC 20230630

Available from: 2023-06-30 Created: 2023-06-30 Last updated: 2023-12-21Bibliographically approved
Alshnakat, A., Lundberg, D., Guanciale, R., Dam, M. & Palmskog, K. (2022). HOL4P4: Semantics for a Verified Data Plane. In: EuroP4 2022: Proceedings of the 5th International Workshop on P4 in Europe, Part of CoNEXT 2022. Paper presented at 5th International Workshop on P4 in Europe, EuroP4 2022, co-located with ACM CoNEXT 2022, Rome, Italy, Dec 9 2022 (pp. 39-45). Association for Computing Machinery (ACM)
Open this publication in new window or tab >>HOL4P4: Semantics for a Verified Data Plane
Show others...
2022 (English)In: EuroP4 2022: Proceedings of the 5th International Workshop on P4 in Europe, Part of CoNEXT 2022, Association for Computing Machinery (ACM) , 2022, p. 39-45Conference paper, Published paper (Refereed)
Abstract [en]

We introduce a formal semantics of P4 for the HOL4 interactive theorem prover. We exploit properties of the language, like the absence of call by reference and the copy-in/copy-out mechanism, to define a heapless small-step semantics that is abstract enough to simplify verification, but that covers the main aspects of the language: interaction with the architecture via externs, table match, and parsers. Our formalization is written in the Ott metalanguage, which allows us to export definitions to multiple interactive theorem provers. The exported HOL4 semantics allows us to establish machine-checkable proofs regarding the semantics, properties of P4 programs, and soundness of analysis tools.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2022
Keywords
formal verification, interactive theorem proving, P4, programming language semantics
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-333491 (URN)10.1145/3565475.3569081 (DOI)001062234700007 ()2-s2.0-85145586258 (Scopus ID)
Conference
5th International Workshop on P4 in Europe, EuroP4 2022, co-located with ACM CoNEXT 2022, Rome, Italy, Dec 9 2022
Note

Part of ISBN 9781450399357

QC 20230802

Available from: 2023-08-02 Created: 2023-08-02 Last updated: 2023-10-16Bibliographically approved
Baumann, C., Dam, M., Guanciale, R. & Nemati, H. (2021). On Compositional Information Flow Aware Refinement. In: 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021): . Paper presented at 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021 (pp. 17-32). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>On Compositional Information Flow Aware Refinement
2021 (English)In: 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021), Institute of Electrical and Electronics Engineers (IEEE) , 2021, p. 17-32Conference paper, Published paper (Refereed)
Abstract [en]

The concepts of information flow security and refinement are known to have had a troubled relationship ever since the seminal work of McLean. In this work we study refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We propose a new epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system's permitted information flows, that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. Our study is set in the context of a class of shared variable multi-agent models similar to interpreted systems in epistemic logic. We demonstrate the expressiveness of our framework through a series of small examples and compare our approach to existing, stricter notions of information-flow secure refinement based on bisimulations and noninterference preservation. Interestingly, noninterference preservation is not supported "out of the box" in our setting, because refinement steps may introduce new secrets that are independent of secrets already present at abstract level. To support verification, we first introduce a "cube-shaped" unwinding condition related to conditions recently studied in the context of value-dependent noninterference, kernel verification, and secure compilation. A fundamental problem with ignorance-preserving refinement, caused by the support for general data and observation refinement, is that sequential composability is lost. We propose a solution based on relational pre- and post-conditions and illustrate its use together with unwinding on the oblivious RAM construction of Chung and Pass.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2021
Series
Proceedings IEEE Computer Security Foundations Symposium, ISSN 1940-1434
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-306541 (URN)10.1109/CSF51468.2021.00010 (DOI)000719322000002 ()2-s2.0-85123687961 (Scopus ID)
Conference
34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021
Projects
trustfullCERCES
Note

Part of conference proceedings ISBN 978-1-7281-7607-9

QC 20211217

Available from: 2021-12-17 Created: 2021-12-17 Last updated: 2024-03-18Bibliographically approved
Dong, N., Guanciale, R. & Dam, M. (2021). Refinement-Based Verification of Device-to-Device Information Flow. In: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021: . Paper presented at Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021. TU Wien Academic Press
Open this publication in new window or tab >>Refinement-Based Verification of Device-to-Device Information Flow
2021 (English)In: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021, TU Wien Academic Press , 2021Conference paper, Published paper (Refereed)
Abstract [en]

I/O devices are the critical components that allow a computing system to communicate with the external environment. From the perspective of a device, interactions can be divided into two parts, with the processor (mainly memory operations by the driver) and through the communication medium with external devices. In this paper, we present an abstract model of I/O devices and their drivers to describe the expected results of their execution, where the communication between devices is made explicit and the device-to-device information flow is analyzed. In order to handle general I/O functionalities, both half-duplex (transmission and reception) and full-duplex (sending and receiving simultaneously) data transmissions are considered. We propose a refinement-based approach that concretizes a correct-by-construction abstract model into an actual hardware device and its driver. As an example, we formalize the Serial Peripheral Interface (SPI) with a driver. In the HOL4 interactive theorem prover, we verified the refinement between these models by establishing a weak bisimulation. We show how this result can be used to establish both functional correctness and information flow security for both single devices and when devices are connected in an end-to-end fashion.

Place, publisher, year, edition, pages
TU Wien Academic Press, 2021
Keywords
Formal verification, Refinement, Serial interface, Device driver, Interactive theorem prover, Information flow
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-303933 (URN)10.34727/2021/isbn.978-3-85448-046-4_21 (DOI)2-s2.0-85123738676 (Scopus ID)
Conference
Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021
Projects
CERCES
Note

Part of ISBN 978-3-85448-046-4

QC 20211117

Available from: 2021-10-29 Created: 2021-10-29 Last updated: 2023-12-21Bibliographically approved
Lundberg, D., Guanciale, R., Lindner, A. & Dam, M. (2020). Hoare-Style Logic for Unstructured Programs. In: Frank de Boer, Antonio Cerone (Ed.), Software Engineering and Formal Methods: . Paper presented at 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020 (pp. 193-213). Cham: Springer Nature
Open this publication in new window or tab >>Hoare-Style Logic for Unstructured Programs
2020 (English)In: Software Engineering and Formal Methods / [ed] Frank de Boer, Antonio Cerone, Cham: Springer Nature , 2020, p. 193-213Conference paper, Published paper (Refereed)
Abstract [en]

Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic , which interprets postconditions relative to program points when these are first encountered. The logic can support both partial and total correctness, derive contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of  have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, making it applicable to the ARMv6 and ARMv8 instruction sets.

Place, publisher, year, edition, pages
Cham: Springer Nature, 2020
Series
LNCS, ISSN 0302-9743, E-ISSN 1611-3349 ; 12310
Keywords
Program logics, Formal verification, Theorem proving, Binary analysis, Hoare Logic
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-281691 (URN)10.1007/978-3-030-58768-0_11 (DOI)000722446400011 ()2-s2.0-85091597792 (Scopus ID)
Conference
18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020
Projects
TrustFullCERCES
Funder
Swedish Foundation for Strategic ResearchSwedish Civil Contingencies Agency
Note

QC 20200921

Available from: 2020-09-21 Created: 2020-09-21 Last updated: 2023-03-30Bibliographically approved
Guanciale, R., Balliu, M. & Dam, M. (2020). InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. In: CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications: . Paper presented at CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, USA, November 9-13, 2020. Association for Computing Machinery (ACM)
Open this publication in new window or tab >>InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis
2020 (English)In: CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications, Association for Computing Machinery (ACM) , 2020Conference paper, Published paper (Refereed)
Abstract [en]

The recent Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. This paper presents such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically, we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of existing countermeasures including constant time and serializing instructions.  

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2020
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-288690 (URN)10.1145/3372297.3417246 (DOI)000768470400110 ()2-s2.0-85096201059 (Scopus ID)
Conference
CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, USA, November 9-13, 2020
Projects
CERCES
Note

QC 20210609

Available from: 2021-01-11 Created: 2021-01-11 Last updated: 2023-03-30Bibliographically approved
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
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-8508, Vol. 9, no 3, p. 243-261Article in journal (Refereed) 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.

Place, publisher, year, edition, pages
Springer, 2019
Keywords
Decomposition, SoC, information flow security, formal verification, hypervisor, ARMv8
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-263686 (URN)10.1007/s13389-019-00216-4 (DOI)000514851500004 ()2-s2.0-85067694646 (Scopus ID)
Projects
CERCES
Funder
Swedish Foundation for Strategic Research
Note

QC 20191111

Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2024-03-18Bibliographically approved
Costa, M., Harrucksteiner, A., Malusà, S., Oggioni, N., Sebastiani, A. & van Dam, B. (2018). A future view on the Nakano district. Stockholm: KTH Royal Institute of Technology
Open this publication in new window or tab >>A future view on the Nakano district
Show others...
2018 (English)Report (Other academic)
Abstract [en]

This project is about reshaping the environment and energy system of Nakano, a residential district inside the city of Tokyo. A qualitative model has been designed, setting the system boundaries and the main features in it. In a second step, ideas about our vision of Nakano in 2040 were developed. The proposed ideas deal with energy, such as the introduction of renewables, but also economics, such as the drop of battery prices, and social well-being, such as the introduction of green areas in the ward.

In our vision for a more sustainable Nakano, a bicycle highway would be introduced and along this, PV panels would be installed to provide shading and electricity generation at the same time. By 2040, cars could represent a service rather than a property. Currently, most of them are fossil-fuel powered and our idea is that this would drastically change. Furthermore, a sustainable car sharing system using autonomous electric vehicles (EVs) was designed. Urban planning has been treated, dealing with converting low-rise buildings into larger apartment buildings to increase the green areas across theward and enhance the building quality. Building quality and performance have also been a core part in the project due to the poor indoor thermal comfort that currently dominates buildings in Nakano.

Economic assumptions for 2040 have been made, especially about price trends for the main technologies introduced in the different scenarios. In order to introduce our ideas in the system and see how they would affect it, we developed four different scenarios, each one generated by different assumptions and energy mixes. These are, Business-as-Usual (BAU), in which current trends are generally followed; Renewable and Nuclear (R&N), where renewables and nuclear are set to be the main actors in the energy supply sector; Zero Nuclear Policy (0-Nuclear), in which nuclear energy has been phased out and, as a consequence, renewables are supposed to meet the entire demand together with the grid; and The Ocean and the Sun (O&S), where nuclear energy is still phased out and ocean energy and large scale solar PV are the new energy sources introduced in the energy mix of the ward.

The whole project was aimed at fulfilling the goals regarding the KPIs. At the end of the report, the results have been shown compared to the original targets. It was proven that reaching every KPI’s target in every scenario was neither technologically nor economically feasible. Anyhow, still a lot of targets were met, and significant improvements compared to today’s conditions of the ward were achieved. Finally, since time is finite, a lot of future work remains that could be a veryinteresting addition to this study about a sustainable future for Nakano.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2018. p. 66
Keywords
Energy management, Systems analysis, Sustainable urban development, LEAP, Homer Pro, IDA ICE
National Category
Energy Engineering Energy Systems Economics
Identifiers
urn:nbn:se:kth:diva-237181 (URN)
Note

This report was written as part of the KTH master's course Energy Management (MJ2410). While it was reviewed by the course instructors and examiner for grading, the results are not considered peer-reviewed. QC 20181024

Available from: 2018-10-23 Created: 2018-10-23 Last updated: 2024-03-15Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0001-5432-6442

Search in DiVA

Show all publications