kth.sePublications
Change search
Link to record
Permanent link

Direct link
Publications (10 of 69) Show all publications
Lundberg, D., Guanciale, R. & Dam, M. (2025). Proof-Producing Symbolic Execution for P4. In: Verified Software. Theories, Tools and Experiments - 16th International Conference, VSTTE 2024, Revised Selected Papers: . Paper presented at 16th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2024, Prague, Czechia, Oct 14 2024 - Oct 15 2024 (pp. 70-83). Springer Nature
Open this publication in new window or tab >>Proof-Producing Symbolic Execution for P4
2025 (English)In: Verified Software. Theories, Tools and Experiments - 16th International Conference, VSTTE 2024, Revised Selected Papers, Springer Nature , 2025, p. 70-83Conference paper, Published paper (Refereed)
Abstract [en]

We introduce a proof-producing symbolic execution tool for formal verification of P4 programs. The tool has been implemented using the interactive theorem prover HOL4 and results are proved sound with respect to the HOL4P4 formalisation of the P4 language. Most notably, this is a general tool for proving functional correctness that can be applied to entire real-world P4 programs.

Place, publisher, year, edition, pages
Springer Nature, 2025
Keywords
Domain-Specific Languages, Formal Verification, Theorem Proving
National Category
Computer Sciences Computer Systems Embedded Systems
Identifiers
urn:nbn:se:kth:diva-363992 (URN)10.1007/978-3-031-86695-1_5 (DOI)2-s2.0-105005252570 (Scopus ID)
Conference
16th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2024, Prague, Czechia, Oct 14 2024 - Oct 15 2024
Note

Part of ISBN 9783031866944

QC 20250603

Available from: 2025-06-02 Created: 2025-06-02 Last updated: 2025-06-03Bibliographically approved
Alshnakat, A., Lundberg, D., Guanciale, R. & Dam, M. (2024). HOL4P4: Mechanized Small-Step Semantics for P4. Proceedings of the ACM on Programming Languages, 8(OOPSLA1), Article ID 102.
Open this publication in new window or tab >>HOL4P4: Mechanized Small-Step Semantics for P4
2024 (English)In: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 8, no OOPSLA1, article id 102Article in journal (Refereed) Published
Abstract [en]

We present the first semantics of the network data plane programming language P4 able to adequately capture all key features of P416, the most recent version of P4, including external functions (externs) and concurrency. These features are intimately related since, in P4, extern invocations are the only points at which one execution thread can affect another. Reflecting P4's lack of a general-purpose memory and the presence of multithreading the semantics is given in small-step style and eschews the use of a heap. In addition to the P4 language itself, we provide an architectural level semantics, which allows the composition of P4-programmed blocks, models end-to-end packet processing, and can take into account features such as arbitration and packet recirculation. A corresponding type system is provided with attendant progress, preservation, and type-soundness theorems. Semantics, type system, and meta-theory are formalized in the HOL4 theorem prover. From this formalization, we derive a HOL4 executable semantics that supports verified execution of programs with partially symbolic packets able to validate simple end-to-end program properties.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2024
Keywords
formal verification, interactive theorem proving, P4, programming language semantics
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-348304 (URN)10.1145/3649819 (DOI)001209927600009 ()2-s2.0-85195797284 (Scopus ID)
Note

QC 20240624

Available from: 2024-06-20 Created: 2024-06-20 Last updated: 2024-06-24Bibliographically approved
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
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0001-5432-6442

Search in DiVA

Show all publications