## Description formal description and verification for access control module
Fixes # (issue) ## Type of change (select or add applied and delete the others) - New feature (non-breaking change which adds functionality) ## How has this been tested? It is formal description for the access control module. It has been proved in Isabelle that the description comply with specifications defined in model.conf. ## Checklist - [ ] Fork the repo and create your branch from `master`. - [ ] If you've added code that should be tested, add tests. - [ ] If you've changed APIs, update the documentation. - [ ] Ensure the tests pass (see CI results). - [ ] Make sure your code lints/format. You can view, comment on, or merge this pull request online at: https://github.com/apache/incubator-teaclave/pull/481 -- Commit Summary -- * draft version of verification code for access control module * Merge remote-tracking branch 'upstream/master' -- File Changes -- A proof/access_control_module/AttrConf.thy (200) A proof/access_control_module/FDP_ACC.thy (99) A proof/access_control_module/FDP_ACF.thy (128) A proof/access_control_module/FDP_IFC.thy (10) A proof/access_control_module/FDP_IFF.thy (55) A proof/access_control_module/FIA_USB.thy (64) A proof/access_control_module/FMT_MSA.thy (167) A proof/access_control_module/InfoType.thy (34) A proof/access_control_module/LEGAL.md (7) A proof/access_control_module/ModelConf.thy (132) A proof/access_control_module/README.md (3) A proof/access_control_module/Resource.thy (12) A proof/access_control_module/ResrcAttr.thy (210) A proof/access_control_module/ResrcType.thy (39) A proof/access_control_module/SysId.thy (21) A proof/access_control_module/TeaclaveAccessControl.thy (149) A proof/access_control_module/TeaclaveRequirements.thy (79) A proof/access_control_module/TrustLevel.thy (28) A proof/access_control_module/UsrAttr.thy (37) A proof/access_control_module/interpretation/I_AttrConf.thy (364) A proof/access_control_module/interpretation/I_FDP_ACC.thy (26) A proof/access_control_module/interpretation/I_FDP_ACF.thy (144) A proof/access_control_module/interpretation/I_FIA_USB.thy (39) A proof/access_control_module/interpretation/I_FMT_MSA.thy (505) A proof/access_control_module/interpretation/I_InfoType.thy (27) A proof/access_control_module/interpretation/I_ModelConf.thy (127) A proof/access_control_module/interpretation/I_ResrcAttr.thy (245) A proof/access_control_module/interpretation/I_ResrcType.thy (50) A proof/access_control_module/interpretation/I_SysId.thy (137) A proof/access_control_module/interpretation/I_TeaclaveAccessControl.thy (32) A proof/access_control_module/interpretation/I_TrustLevel.thy (29) A proof/access_control_module/interpretation/I_UsrAttr.thy (30) -- Patch Links -- https://github.com/apache/incubator-teaclave/pull/481.patch https://github.com/apache/incubator-teaclave/pull/481.diff -- 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/pull/481
