3 ms·
Or if you want to go in the complete opposite direction, formal proofs of your system down to the binary, look at seL4.
by hga 11y ago
Or if you want to go in the complete opposite direction, formal proofs of your system down to the binary, look at seL4.
- pgeorgi 11y agoSo you have a formally verified kernel. And then what? It's possible to run L4 processes written in SPARK on top of seL4.
- hga 11y agoMy suggestion of a wildly different approach was to more or less replicate what NICTA et. al. did with seL4 with your own project. There's also the Coq ecosystem, which includes a verified free for non-commercial use C compiler.
- pgeorgi 11y agoThat's possible, but incredibly tedious. It may be easier to just generate binary code from assembly in coq (as Microsoft Research has demonstrated: http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...) instead of trying to shoehorn a C compiler into a verified context and then running proofs over that for non-trivial problems. seL4 was a huge project. Once you start reasoning about using L4 APIs, it will only become worse (eg. it's not simple to determine who has access to the pages in any L4 AddressSpace)