> Thanks for your proposal. Sorry for the late reply. Can you provide a simple > example to clarify your goal. More specifically, I'd like to see what kind of > outputs you will contribute (e.g., formal document, proof, and readme to > reproduce). Please try your best to list them. The followup question is about > how to integrate your contributions into the project. If you have can provide > several sample repositories on how to open source specifications, that would > be very helpful.
The outputs of my work include: 1. atomized decomposition of access control module based on CC(common criteria),along with the standardized documentation 2. formal representation of specification of the access control module constructed by decomposed components 3. formal representation of security objectives required by model.conf 4. mechanic proof with readable steps showing that the specification complies with the security objectives. Isabelle/Isar/HOL is used as a programing language for the formal presentation. The specification is constructed using built-in module called locale of Isabelle. The consistency proof between specifications is also proved using interpretation mechanism. For the explanation of the mechanism provided by Isabelle, such as locale, please refer to: https://isabelle.in.tum.de/documentation.html. As for open sourced specifications, links below might be helpful: https://github.com/ZipCPU/wbuart32/tree/master/doc -- You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub: https://github.com/apache/incubator-teaclave/issues/453#issuecomment-763590299
