Hi Oak, Norrathep Rattanavipanon wrote:
What I'm missing is the generated theorems provided by CAmkES. I'm looking for something similar to chapter 5 and Appendix B of this technical report:
The proofs for the C glue code have not been maintained, and no longer work with the latest CAmkES version. Additionally, the proofs only covered some interfaces. We don't have a timeline for reviving the C proofs in the foreseeable future. You can still find the templates under `camkes-tool/camkes/templates/autocorres`. The last known working branch is archived on our Repo manifest. Use the branch `FM2015`: repo init -b FM2015 https://github.com/seL4/camkes-manifest This will also require a contemporary version of l4v. We are exploring how to verify glue code written in CakeML (https://cakeml.org), which ties in with our active efforts to use CakeML on seL4. Hope this clarifies things.
Roughly speaking, our plan is to use: (1) Isabelle theorems generated by the CapDL capability distribution framework to prove isolation of the user-space and (2) the CAmkES generated Isabelle theorems to prove functional correctness of our security-critical user-space process. The operations of our security-critical process should be simple and similar to the quoting enclave in SGX
If the program is simple, it might be feasible to perform the relevant proofs by hand. One difficulty is that the latest C glue code might not conform to our formal C subset and would need to be tweaked. Aside from that, the proofs should be conceptually similar. Good luck with your project. Cheers, Japheth Lim Proof Engineer, Trustworthy Systems