SWEN90010 – High Integrity
Systems Engineering
Alloy Example and Trace-Based Modelling (Capability-Based Access Control)
Copyright By PowCoder代写 加微信 powcoder
DMD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray
ACCESS CONTROL
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Access Control
who can access what in which ways
the “who” are called subjects e.g. users, processes etc.
the “what” are called objects
e.g. individual files, sockets, processes etc.
includes all subjects
the “ways” are called permissions
e.g. read, write, execute etc.
are usually specific to each kind of object
include those meta-permissions that allow modification of the
protection state
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
AC Mechanisms and Policies
Specifies allowed accesses
And how these can change over time AC Mechanism
Implements the policy
Certain mechanisms lend themselves to certain kinds of policies
Certain policies cannot be expressed using certain mechanisms
Protection State
Access control matrix defines the protection state at any instant in time
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Storing Protection State
Not usually as access control matrix too sparse, inefficient
Two obvious choices:
store individual columns with each object
defines the subjects that can access each object
each such is called the subject’s capability list
each such column is called the object’s access control list defines the objects each subject can access
store individual rows with each subject
Access Control Lists (ACLs)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Subjects usually aggregated into classes e.g. UNIX: owner, group, everyone
Meta-permissions (e.g. own) control class membership
allow modifying the ACL
Implemented in almost all commercial OSes
Capabilities
A capability is a capability list element
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Names an object to which the capability refers Confers permissions over that object
Less common in commercial systems More common in research though
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Capabilities: Implementations
Capabilities must be unforgeable On conventional hardware, either:
Stored as ordinary user-level data, but unguessable due to sparseness like a password or an encryption key
like UNIX file descriptors
Sparse capabilities can be leaked more easily, but are easier to revoke
The only solution for most distributed systems
Stored separately (in-kernel), referred to by user programs by index/
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Mandatory vs. Discretionary AC
Discretionary Access Control:
Users can make access control decisions delegate their access to other users etc.
Mandatory Access Control (MAC): enforcement of administrator-defined policy
users cannot make access control decisions (except those allowed by
mandatory policy)
can prevent untrusted applications running with user’s privileges from
causing damage
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Common in areas with global security requirements e.g. national security classifications
Less useful for general-purpose settings: hard to support different kinds of policies
all policy changes must go through sysadmin
hard to dynamically delegate only specific rights required at runtime
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Bell-LaPadula (BLP) Model
MAC Policy/Mechanism
Formalises National Security Classifications
Every object assigned a classification e.g. TS, S, C, U
Classifications ordered in a lattice e.g. TS > S > C > U
Every subject assigned a clearance
Highest classification they’re allowed to learn
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
BLP: Rules
Simple Security Property (“no read up”):
s can read o iff clearance(s) >= class(o)
S-cleared subject can read U,C,S but not TS standard confidentiality
*-Property (“no write down”):
s can write o iff clearance(s) <= class(o)
S-cleared subject can write TS,S, but not C,U
to prevent accidental or malicious leakage of data to lower levels
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Boebert’s Attack
Boebert 1984: “On the Inability of an Unmodified Capability Machine to
Enforce the *-Property“
Shows an attack on sparse capability systems that violates the *-property Where caps and data are indistinguishable
Does not work against partitioned capability systems Practically all capability-based kernels
LET’S MODEL THIS IN ALLOY
Initial Conditions for Attack
Low RW LoSeg rw_l
16 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
What we need to model Data
Capabilities: each points to an object and carries certain access rights (permissions)
Objects: things capabilities point to; each has a classification (High or Low)
Actors (i.e. programs): that can use capabilities that they possess
Memory Segments: which store Data
17 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Boebert’s Attack
r_l.read()
High R rw_l.write(rw_l) RW r_l R
Low RW LoSeg rw_l rw_l
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Low writes his cap into the low segment from which High reads it out
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Boebert’s Attack: Lessons
Not all mechanisms suited to all policies
Many policies treat data- and access-propagation differently
BLP is one example
Cannot be expressed using sparse capability systems
This does not mean that capability systems and MAC are incompatible in
TRACE-BASED MODELLING IN DETAIL
Trace-Based Modelling
Can’t just consider individual state transitions:
We to talk about a sequence (aka a trace)
of such transitions.
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Trace (Sequence of States) s1 s2 s3 s4...
There is a state transition between each pair of states in the sequence
How do we define this in Alloy?
22 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Traces in Alloy
Alloy 6 natively reasons about traces
The models (behaviours) that Alloy considers (e.g. when doing check and run)
are lasso traces
23 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Defining Traces
We need to give these traces meaning
Constrain the state transitions:
fact trans { always all s: State |
op1[s] or op2[s] or ... or unchanged[s] } (Often, also) constrain the first state:
fact init { all s: State | init[s] }
24 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com