CS代考 SWEN90010 – High Integrity – cscodehelp代写

SWEN90010 – High Integrity
Systems Engineering
Alloy Example and Trace-Based Modelling (Capability-Based Access Control)

Copyright By cscodehelp代写 加微信 cscodehelp

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代考 加微信: cscodehelp QQ: 2235208643 Email: kyit630461@163.com