tree: d551b4ee6411daf467cc6b9af1013fb8f9349542 [path history] [tgz]

# Formal description and verification for access control module

## Motivation

The Vulnerabilities of an IT product, such as teaclave access control module, are often caused by the failures in the compliance between requirements and specifications. In order to achieve high confidence of teaclave access control module, the formal description of specification and requirements is required to eliminate the ambiguity introduced by natural language. Moreover, the formal verification is also required to show the compliance between specifications and requirements.

## Introduction

Instead of modeling code directly, the formal language used here describes the design/specifications of access control module and the requirements written in model.conf. To be more specific, the specifications are composed by a set of security functional requirements, also known as SFR. Algebra structure is used for constructing each security functional requirement. The requirements are formalized by the primitives declared in specifications. The proof procedure is to show the compliance between requirements and specifications.

## Prerequisite

To completely understand the design principle and the semantics of formal language used here, learning Isabelle and Common Criteria is required. If you are familiar with Isabelle and Common Criteria, you can skip this section.

### Isabelle

Isabelle is a generic proof assistant. To learn the main concept, syntax and others of Isabelle, please refer to `isabelle tutorial`.

The specifications are constructed using locale and interpretation provided by Isabelle. To learn more about locale and interpretation, please refer to `locale and interpretation tutorial`.

### Common Criteria

Common Criteria for Information technology is an international standard for the evaluation of Security of products. It documents a set of security functional requirements which is used for decomposing the requirements. The requirements of teaclave access control module is decomposed based on the security functional requirements. For the description of security functional requirements, please refer to `Common Criteria part 2`.

### Algebra structures

In mathematics, an algebraic structure consists of a nonempty set A, a collection of operations on A of finite arity, and a finite set of identities, knowns as axioms, that these operations must satisfy. This can be used for constructing programs if nonempty set is considered as data structure or type, operations are considered as functions and axioms are considered as function contracts that must be obeyed. For more information, please refer to `wiki`.

## Setup

To open and build the repository, Isabelle engine and IDE are required. Once the `Isabelle and IDE` are installed and the repository is `imported into IDE`, the repository will be built and proved automatically.

## Overview

The repository is organised as follows.

### Specification

As stated before, the design of teaclave access control module are formalized using locales. The description of teaclave access control module is in `TeaclaveAccessControl.thy`. This is the “main” description of access control module. The primitives used for description are located in other files. The general description of the purpose of each file used for composing the “main” description of access control module is listed as follows:

• `AttrConf.thy`: This works as a common structure for describing successive structures, such as list, array and so on. It will be imported to other structures.

• `InfoType.thy`: This is used for describing the objects to be accessed. It corresponds to the objects described in `access-control.md`. Enumeration type can be considered as a concrete example for this structure.

• `SysId.thy`: This is used for describing Ids required by the specification of access control module. It works as an attribute of entities involved in the access control module.

• `TrustLevel.thy`: This is used for describing the location of entities. It works as an attribute of entities involved in the access control module.

• `ResrcType.thy`: This is used for describing the type of resources used by access control module. It works as an attribute of entities involved in the access control module.

• `UsrAttr.thy`: This is used for describing user attribute of access control module.

• `ResrcAttr.thy`: This is used for describing attributes of different entities. The entities include subject, object and information.

• `FDP_ACF.thy`: This is used for describing the security functional requirement identified by `FDP_ACF:USER DATA PROTECTION-Access control functions` in Common Criteria. It works as a component to construct the access control module.

• `FIA_USB.thy`: This is used for describing the security functional requirement identified by `FIA_USB:IDENTIFICATION AND AUTHENTICATION-User subject binding` in Common Criteria. It works as a component to construct the access control module.

• `FMT_MSA.thy`: This is used for describing the security functional requirement identified by `FMT_MSA:SECURITY MANAGEMENT-Management of security attributes` in Common Criteria.It works as a component to construct the access control module.

• `ModelConf.thy`: This is used for describing the configuration file required by access control module.

• `FDP_ACC.thy`: This is used for describing the security functional requirement identified by `FDP_ACC:USER DATA PROTECTION-Access control policy` in Common Criteria. It works as a component to construct the access control module.

### Requirement

The requirements are formalized and proved in `TeaclaveRequirements.thy`. This is the formal proof based on the access control module description. It shows that the description complies with the specifications required by the access control module.

### `Interpretation`

The axioms described in locales might not be consistent. In order to ensure the consistency between different axioms, an instance is provided for each locales. The interpretation can also be considered as the implementation of access control module in Isabelle.

## Future work

The formal description along with the verification only shows the compliance between requirements and specifications. The compliance between specification and implementation remain unsolved. Fortunately, the axioms described in locales can be used as inputs to write test cases following MC/DC procedure. In the future, the test cases based on axioms and MC/DC will be provided. With the help of test cases and structural coverage analysis, it is adequate to show the compliance between specification and implementation, so is the compliance between requirements and implementation. Except for access control module, the formal description, verification and test cases will be provided to other modules.