3 ms·
no, just no. SDV uses model checking and symbolic execution. its exploration is partial. the guarantees you get from the rust type checker are much stronger.
by munin 11y ago
no, just no.
SDV uses model checking and symbolic execution. its exploration is partial. the guarantees you get from the rust type checker are much stronger.
the real trick would be, could you represent the contract between the kernel and drivers as rust types. if you could, then you don't need SDV, you just need the rust type checker.
- nickpsecurity 11y agoThat would be a real trick. Meanwhile, the reality is Microsoft's tools cover more stuff in this area. That blue screens are rare speaks to tge results. Make sonething equivalent for Rust then we'll talk along these lines.
- ulber 11y agoSDV proves properties that are in general undecidable, and as such it is not possible to substitute the Rust type checker for it. The critical difference is that software verification algorithms are allowed to be partial (i.e. not terminate or return "unknown"), while type checking algorithms are required to be total. Edit: Another way to look at it is that software verification tools find proofs for properties, while type checkers only verify proofs (given as the program structure and type annotations).
- geon 11y agoBut couldn't the type system guarantee a sufficent subset of all the possible interactions with the api? Like, you can't determine the halting problem for a turing complete language, but you can for s more restricted language.
- ulber 11y agoOne option which allows you to keep Turing completeness is just asking the user to write more annotations, such as loop invariants and termination conditions. For example the Dafny [1] language+verifier does this: it automates the tedious parts of the proofs but requires the user to give the hard parts (loop invariants) as annotations. [1]: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/