The access control module plays a key role in the teaclave architecture, it works as a base security function for other functions to use in teaclave. Because of that, the vulnerabilities of access control module can cause severe threats which breaks down the whole system. So, it is necessary to provide rigorous evidences showing that the implementation of access control policy complies with the security objectives required.
In order to achieve the rigorous compliance between implementation and security objectives required, I propose formal specification and verification for tealcave access control module in Isabelle. Here is a brief summary of steps to achieve this: 1. identify the security objectives required by teaclave access control module 2. decompose the security objectives to security functional requirements(SFR) based on CC (common criteria for information technology) 3. use axioms and uninterpreted types, constants, and functions as formal specifications in terms of SFR to represent the system architecture and high level design of teaclave access control module 4. state the security objectives as theorems in the context of formal specifications created in step 3. 5. demonstrate by proving with Isabelle that the security objectives specified as theorems are satisfied by the formal specifications created in step 3. After the steps above, the verified formal specifications are provided. The axioms used for constructing the formal specifications can then be used to verify the implementation by creating test cases following MC/DC procedure. There are many other base security function modules in teaclave. In the future, I hope to provide formal specification and verification for all such modules. -- 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
