Open this publication in new window or tab >>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
2023-06-302023-06-302023-12-21Bibliographically approved