Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2501.00248 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929653798666240 |
|---|---|
| author | Ijaz, Ramla Boos, Kevin Zhong, Lin |
| author_facet | Ijaz, Ramla Boos, Kevin Zhong, Lin |
| contents | This paper reports our experience of providing lightweight correctness guarantees to an open-source Rust OS, Theseus. First, we report new developments in intralingual design that leverage Rust's type system to enforce additional invariants at compile time, trusting the Rust compiler. Second, we develop a hybrid approach that combines formal verification, type checking, and informal reasoning, showing how the type system can assist in increasing the scope of formally verified invariants. By slightly lessening the strength of correctness guarantees, this hybrid approach substantially reduces the proof effort. We share our experience in applying this approach to the memory subsystem and the 10 Gb Ethernet driver of Theseus, demonstrate its utility, and quantify its reduced proof effort. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_00248 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Combining Type Checking and Formal Verification for Lightweight OS Correctness Ijaz, Ramla Boos, Kevin Zhong, Lin Operating Systems This paper reports our experience of providing lightweight correctness guarantees to an open-source Rust OS, Theseus. First, we report new developments in intralingual design that leverage Rust's type system to enforce additional invariants at compile time, trusting the Rust compiler. Second, we develop a hybrid approach that combines formal verification, type checking, and informal reasoning, showing how the type system can assist in increasing the scope of formally verified invariants. By slightly lessening the strength of correctness guarantees, this hybrid approach substantially reduces the proof effort. We share our experience in applying this approach to the memory subsystem and the 10 Gb Ethernet driver of Theseus, demonstrate its utility, and quantify its reduced proof effort. |
| title | Combining Type Checking and Formal Verification for Lightweight OS Correctness |
| topic | Operating Systems |
| url | https://arxiv.org/abs/2501.00248 |