Formally verifying properties of the Blinded Memory architecture using F*

Description

The Blinded Memory (BliMe) extensions enforce a security property based on information flows: the observable system state, including state observable by side channels, must be independent of any sensitive data stored in the system. Achieving this requires modifications to every instruction in the architecture. Given the breadth of these changes, we want to ensure that the changes that we plan to make are really sufficient to enforce our security property. We achieve this by building a formal model using the F* language. Well-known for its use in the formally-verified HACL* cryptographic library and miTLS TLS implementation, F* is a dependently-typed functional language in the ML family that can verify program properties with the aid of SMT. We use F* to build a model of a simple CPU incorporating BliMe, and show that it enforces our information flow property. In this talk we will present a brief introduction to the F* language, and show how we used it to prove the correctness of our model of a BliMe-supporting CPU.

Aikajakso	22 elok. 2023
Tapahtuman otsikko	Summer School on System Security
Tapahtuman tyyppi	Conference
Sijainti	Saarbrücken, Saksa, SaarlandNäytä kartalla