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 _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
