Tracking formal verification status

future-proof-iot / RIOT-rs

RIOT-rs is an operating system for secure, memory-safe, low-power Internet of Things, written in Rust

Apache License 2.0

32 stars 12 forks source link

Tracking formal verification status #140

Open emmanuelsearch opened 4 months ago

emmanuelsearch commented 4 months ago

Based on the current use of hax and with regards to our draft manifesto, the question arises of where/how to track where we currently are at, now that initial integration has begun e.g. with #126.

emmanuelsearch commented 4 months ago

to give a concrete example: based on https://github.com/future-proof-iot/RIOT-rs/blob/main/src/riot-rs-runqueue/proofs/fstar/extraction/Makefile how/where should we express (for laypeople) what verification(s) are currently provided by CI for the scheduler? @W95Psp @franziskuskiefer obviously we'd very much value your suggestions on this ;)

franziskuskiefer commented 4 months ago

So do we have panic freedom already? If yes, then you should think about the contracts (pre- and post-conditions) the functions have and if there's something interesting that should be proven. In parallel, adding more crates to the extraction, lax typechecking, etc. pipeline.

To the documentation, I think panic freedom should be documented when the extracted code typechecks in F*. Additional properties should then come from the contracts the functions get and get described accordingly.

emmanuelsearch commented 4 months ago

@franziskuskiefer thanks for the input. A more basic question then: what is the fundamental difference between typechecking and lax typechecking ? (I seem to remember @W95Psp hinting that RunQueue was lax typechecking already, but I am not sure if my memory plays tricks on me, or how to check that myself ;)

franziskuskiefer commented 4 months ago

I think the easiest description is

lax typechecking -> valid F* code is generated and all dependencies (like from the Rust core library) are defined
typechecking -> panic freedom (F* proved that no panic occurs in the code)

ROMemories commented 3 months ago

@W95Psp Could you detail the steps that would now be required to typecheck the riot-rs-runqueue crate and prove panic-freedom? The hax.yml CI workflow currently only does lax typechecking if I understand correctly.