| commit | 566a295590a4d9040a2e330a35f832673aa93365 | [log] [tgz] |
|---|---|---|
| author | SeanVer <77425230+SeanVer@users.noreply.github.com> | Sun Jan 30 04:12:29 2022 +0800 |
| committer | GitHub <noreply@github.com> | Sat Jan 29 12:12:29 2022 -0800 |
| tree | 65ed148d30068382ab3c54b7b53cb2ad143c2236 | |
| parent | 7e2a7a61fc15e0af4d877e124b4700e77637cc7a [diff] |
extra lemma proof and redundant proof procedure deletion (#5) Signed-off-by: Cao Shuang <caoshuang.cs@antfin.com> Co-authored-by: 小狈 <caoshuang.cs@antgroup.com>
This repository contains formal descriptions, specifications, and proofs for Teaclave.
access_control_moduleThis directory contains formal description and verification of access control module of Teaclave described in access-control.md. It uses security functional requirements to restate the design specifications, then proves the required security objectives in Isabelle.
The purpose of security problem definition is to identify the scope of problems to be solved by the access control module. The security problem of access control module of Teaclave is defined in terms of the assets protected by the module, the threats encountered by the module and the preconditions assumed to be true to the module.
Assets: the confidentiality and integrity of critical data operated by the tasks and functions defined by Teaclave
Threats: runtime tasks and functions abuse which compromise the confidentiality and integrity of critical data.
Assumptions: the critical data can only be accessed through tasks and functions defined by Teaclave; the identification and authentication of users is achieved by the other modules of Teaclave.
The security objective of access control module is to prevent unauthorized users from accessing the critical data through tasks and functions. By achieving the security objective, the threats of runtime tasks and functions abuse are eliminated under the assumptions identified in security problem definition.
Security functional requirements of Common Criteria are used for decomposing security objectives with standardized language. The security objective of Teaclave access control module is decomposed as follows:
FIA_UAU.2 User authentication before any action
Dependencies：FIA_UID.1 timing of identification
FIA_UID.2 User identification before any action
Dependencies：No dependencies
FIA_UAU.3 Unforgeable authentication
Dependencies：No dependencies
FIA_UAU.3.1 The Teaclave access control module shall prevent use of authentication data that has been forged by any user of the Teaclave access control module. (This requirement is already covered by assumption, so it is not formalized.)
FIA_UAU.3.2 The Teaclave access control module shall prevent use of authentication data that has been copied from any other user of the Teaclave access control module. (This requirement is already covered by assumption, so it is not formalized.)
FIA_USB.1 User-subject binding
Dependencies：FIA_ATD.1 User attribute definition
FIA_USB.1.1 The Teaclave access control module shall associate the following user security attributes with subjects acting on the behalf of that user: UsrId.
FIA_USB.1.2 The Teaclave access control module shall enforce the following rules on the initial association of user security attributes with subjects acting on the behalf of users: UsrId is in the participants of subjects.
FIA_USB.1.3 The Teaclave access control module shall enforce the following rules governing changes to the user security attributes associated with subjects acting on the behalf of users: None.
FIA_ATD.1 User attribute definition
Dependencies：No dependencies
FDP_ACC.1 Subset access control
Dependencies：FDP_ACF.1 Security attribute based access control
FDP_ACF.1 Security attribute based access control
Dependencies：FDP_ACC.1 Subset access control；
FMT_MSA.3：Static attribute initialisation
FDP_ACF.1.1 The Teaclave access control module shall enforce the Teaclave Subset access control SFP to objects based on the following:
subject attributes: task_participant; UsrId
object attributes: function_owner; data_owner.
FDP_ACF.1.2 The TSF shall enforce the following rules to determine if an operation among controlled subjects and controlled objects is allowed:
task_access_data is allowed if data_owner is the subset of task_participant;
task_access_function is allowed if function_owner is the subset of task_participant;
user_access_data is allowed if UsrId is in data_owner;
user_access_function is allowed if UsrId is in function_owner.
FDP_ACF.1.3 The TSF shall explicitly authorize access of subjects to objects based on the following additional rules: NONE.
FDP_ACF.1.4 The TSF shall explicitly deny access of subjects to objects based on the following additional rules: NONE.
FMT_MSA.3 Static attribute initialization
Dependencies：FMT_MSA.1 Management of security attributes；
FMT_SMR.1 Security roles
FMT_MSA.3.1 The Teaclave access control shall enforce the Teaclave Subset access control SFP to provide permissive default values for security attributes that are used to enforce the SFP.
FMT_MSA.3.2 The TSF shall not allow the Users to specify alternative initial values to override the default values when an object or information is created.
FMT_MSA.1 Management of security attributes
Dependencies：FDP_IFC.1 Subset information flow control；
FMT_SMR.1 Security roles；
FMT_SMF.1 Specification of Management Functions
FMT_SMR.1 Security roles
Dependencies：FIA_UID.1 Timing of identification
FMT_SMR.1.1 The Teaclave access control module shall maintain the roles: User.
FMT_SMR.1.2 The Teaclave access control module shall be able to associate users with roles.
FMT_SMF.1 Specification of Management Functions
Dependencies：No dependencies
Each security functional requirement listed above is formalized and located in different files. For more information, please refer to access control module introduction.