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>
3 files changed
tree: 65ed148d30068382ab3c54b7b53cb2ad143c2236
  1. access_control_module/
  2. .travis.yml
  3. README.md
README.md

Build Status

Teaclave Verification

This repository contains formal descriptions, specifications, and proofs for Teaclave.

access_control_module

This 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.

security problem definition

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.

security objectives

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 requirements

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_UAU.2.1 The Teaclave access control module shall require each user to be successfully authenticated before allowing any other Teaclave-mediated actions on behalf of that user. (This requirement is already covered by assumption, so it is not formalized.)
  • FIA_UID.2 User identification before any action
    Dependencies:No dependencies

    • FIA_UID.2.1 The Teaclave access control module shall require each user to be successfully identified before allowing any other Teaclave-mediated actions on behalf of that user. (This requirement is already covered by assumption, so it is not formalized.)
  • 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

    • FIA_ATD.1 The Teaclave access control module shall maintain the following list of security attributes belonging to individual users: UsrId.
  • FDP_ACC.1 Subset access control
    Dependencies:FDP_ACF.1 Security attribute based access control

    • FDP_ACC.1.1 The Teaclave access control module shall enforce the Teaclave Subset access control SFP on:
      subject: task, user;
      object: function, data;
      operation: task_access_data, task_access_function, user_access_data, user_access_function.
  • 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_MSA.1.1 The Teaclave access control module shall enforce the Teaclave Subset access control SFP to restrict the ability to query the security attributes to Users.
  • 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

    • FMT_SMF.1.1 The Teaclave access control module shall be capable of performing the following management functions:
      request_user_access_data, request_user_access_function, request_task_access_data, request_task_access_function, request_user_access_task.

Each security functional requirement listed above is formalized and located in different files. For more information, please refer to access control module introduction.