Security Policy

Introduction

This example demonstrates how to specify a system specification.

Natural Language Description

We consider a smart card that we want to certify at EAL5+ level. It is necessary to model the security policy and to verify by proof that it is consistent.
We define:
  • the objects implemented in the security policy and
  • the expected security properties,
in terms of access rights to the various memories according to the type of process executing a given operation.

Global model

  • Representing the operation of the CPU, MPU memory system
  • Focused on memory access management

Objects

process mode USER or SUPERVISOR tMODE
memory type RAM, PUBLIC ROM or SECURE ROM tMEMORY
memory content DATA or CODE tCONTENT
operation READ, WRITE or EXECUTE tOPERATION
access GRANTED or NOT GRANTED tRESULT

Implementation of the security policy

Each time an attempt is made to perform an operation to a memory slot for a process mode, then the access is:
  • either allowed (GRANTED) or
  • not yet allowed (NOT GRANTED)

Modelling principles

The memory is abstract (we do not manipulate addresses but memory cells): abstract set MEMORY.
Indication functions allow to associate to each memory cell
  • Its type (memory map): MEMORY_TYPE : MEMORY --> tMEMORY
  • Its content: MEMORY_CONTENT : MEMORY --> tCONTENT
Four variables are defined:
  • currentCell currentCell : MEMORY
  • currentOperation currentOperation : tOPERATION
  • currentMode currentMode : tMODE
  • currentResult currentResult : tRESULT
Properties are permanently checked by these four variables.
Below is the skeleton of the B machine politique.mch:
1
MACHINE politique
2
SETS
3
MEMORY;
4
tMEMORY={RAM, ROM_SECURE, ROM_PUBLIC};
5
tCONTENT={DATA, CODE};
6
tMODE={USER, SUPERVISOR};
7
tOPERATION={OP_READ, OP_WRITE, OP_EXECUTE, OP_NONE};
8
tRESULT={GRANTED, NOT_GRANTED}
9
CONSTANTS
10
MEMORY_TYPE, MEMORY_CONTENT
11
PROPERTIES
12
MEMORY_TYPE : MEMORY --> tMEMORY &
13
MEMORY_CONTENT : MEMORY --> tCONTENT
14
VARIABLES
15
currentCell, currentOperation, currentMode, currentResult
16
INVARIANT
17
currentCell : MEMORY &
18
currentOperation : tOPERATION &
19
currentMode : tMODE &
20
currentResult : tRESULT
21
INITIALISATION
22
currentCell :: MEMORY ||
23
currentOperation :: tOPERATION ||
24
currentMode :: tMODE ||
25
currentResult :: tRESULT
26
OPERATIONS
27
Init =
28
ANY cell, operation WHERE
29
cell : MEMORY &
30
operation : tOPERATION
31
THEN
32
currentCell := cell ||
33
currentOperation := operation ||
34
currentResult := NOT_GRANTED
35
END;
36
​
37
ChangeMode =
38
ANY mode WHERE
39
mode : tMODE & not(mode=currentMode) &
40
currentOperation = OP_EXECUTE &
41
currentResult = GRANTED
42
THEN
43
currentMode := mode
44
END
45
END
Copied!
This specification needs to be completed with more operations and invariants. One operation and one invariant are given below.

operation EXECUTE access in RAM:

If the current memory location is RAM, the memory cell contains CODE, and the current operation is EXECUTE, then access is granted.
1
executeRAM =
2
SELECT
3
MEMORY_TYPE(currentCell) = RAM &
4
MEMORY_CONTENT(currentCell) = CODE &
5
currentOperation = OP_EXECUTE
6
THEN
7
currentResult := GRANTED
8
END
Copied!

invariant ROM_SECURE out of reach from USER

A memory cell of type ROM_SECURE can only be read in SUPERVISOR mode.
1
MEMORY_TYPE(currentCell)=ROM_SECURE &
2
currentOperation = OP_READ &
3
currentMode = USER
4
=>
5
currentResult = NOT_GRANTED
Copied!
: