formal specification and verification for teaclave access control module

[SeanVer]

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.

[mssun]

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.

[SeanVer]

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