CSC8204
Secure Software Development
Coursework 2023
Aims:
The aim of this assignment is to increase and assess understanding and resolution of risk analysis,
SecureUML design, formal modelling and verification.
The coursework consists of 4 equally weighted questions.
Submission details:
Submission deadline: 15 Dec 2023, 15:30
Submit your solution to Ness by the deadline. Your solution should consist of a single .docx or
.pdf document with answers to each of the questions below.
Assessment:
The coursework is marked out of 100, with 25 marks for each question .
Support:
You will find the formative exercises in Dafny and SecureUML useful for answering the
questions in this coursework. After completing these exercises, you can use the remaining
practical classes to ask questions.
Questions can also be posted in the Canvas discussion board.
Scenario:
This coursework is derived from the Tokeneer ID Station, a research project undertaken in 2008
by Altran Praxis (formerly Praxis Critical Systems). The project was to demonstrate the
development of secure systems in a rigorous manner, and the final report1 provides an overview
of the project documentation, including requirements analysis, formal specification (in Z),
SPARK Ada implementation and verification, and top-down system testing.
Tokeneer is described as a “biometrics prototype”. The Tokeneer ID Station or TIS, one part of
the Tokeneer System, protects access to secure information held on a network of workstations,
held in a physically secure space or “enclave”.
1 Available from AdaCore at http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf
Figure 1 Tokeneer system overview
The Tokeneer system displayed in Figure 1 consists of the secure enclave plus other components
that are physically either inside or outside the enclave:
• Enrolment Station issues a token to a user. The token contains up to four signed
certificates: an ID Certificate generated by a Certificate Authority; a Privilege Certificate
and a biometric Identification and Authentication (I&A) Certificate, both generated by an
Attribute Authority; and an Authorisation Certificate which is generated by the TIS, as
described below.
• Tokeneer ID Station (TIS) uses the biometric information in the I&A certificate, and
scan of the user’s fingerprint, to verify the user. On successful identification, if the
Privilege Certificate confirms the user has sufficient clearance, the TIS adds a signed
Authorisation Certificate to the user’s token and releases the enclave door lock, allowing
entrance to the secure space.
• Inside the secure space (enclave) are a number of Workstations. A workstation checks
the Authorisation Certificate to confirm the user is currently authorised to use the
workstation facilities.
Part A Applied Risk Analysis [25 Marks]
According to McGraw’s software security approach, the secure software development is founded
on a comprehensive applied risk analysis taking into account business goals, business risks, and
technical risks.
Aim:
Develop an applied risk analysis based on the documentation of the Tokeneer project
(http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf).
Approach:
Develop the risk analysis based on McGraw’s methodology introduced in the recommended
literature McGraw – Software Security and in the lecture on Principles of Software Security.
Evaluate:
1. Business goals of Praxis High Integrity Systems in undertaking the Tokeneer project.
Rank the business goals according to the NIST business goal classification.
2. Three main business risks affecting Praxis High Integrity Systems, including:
• Business risk indicator
• NIST business risk likelihood scaling
• NIST business risk impact scaling
• Overall NIST severity ranking.
• A one-sentence rationale, why you have chosen this risk over others.
3. Five main technical risks determinable from the Tokeneer report and software
deliverable.
• Analyze the software artifacts
• Evaluate the software security touchpoints
• Use the 10 best practice security principles by McGraw.
• Specify the risk likelihood and possible impact vis-à-vis of available controls.
• Write a one-sentence rationale, why you have chosen this risk over others.
4. Conduct a risk synthesis connecting business goals, business risks and technical risks.
5. Derive one mitigation approach for each technical risk. Justify your choice.
Deliverable:
To complete this part of the coursework, complete an applied risk management report that
enumerates the risk register in the tabular form introduced by McGraw and in the lecture on
Principles of Software Security. Examples for such tables are given in the lecture slides, slides
27-39.
In addition to the risk register, document the rationale for the risks and the chosen mitigation
methods in a brief summary, no more than one side A4.
Ultimately, the coherence and consistency of your argument for your choices will be key in
achieving high marks. The risks and mitigation methods must fit the indicated Tokeneer scenario.
Indicative marking guidance: business goals and risks [5 Marks], technical risks [10 Marks], risk
synthesis and mitigation [5 Marks], rationale [5 Marks].
Part B SecureUML Design [25 Marks]
Model-driven security (MDS) embeds security controls into generated source code and enables
formal verification. We investigate SecureUML as a an MDS approach that enables enforcement
of confidentiality and integrity through Role-Based Access Control (RBAC).
Aim:
Develop a high-level UML model in the style of SecureUML which models a suitable security
policy for the Tokeneer ID station.
Figure 2 SecureUML Metamodel
Approach:
Create an UML Class model that takes the SecureUML metamodel shown in Figure 2 as
foundation and models as a mock-up the defined security policy. Do this in IntelliJ IDEA
Diagrams or another appropriate UML modelling software (e.g., Papyrus or Eclipse Modelling).
Design:
Design an UML diagram in the fashion of SecureUML to model the following authentication
system: The system manages the certificate handling of the Tokeneer ID station, including (i)
how superusers can grant and revoke certificates, (ii) how certificates are derived from one
another, and (iii) how an enclave user can log in to and be logged out from workstations.
Create a UML design to capture the following security policy: Subjects = { Alice, Bob,
Administrator }; Roles = { EnclaveUser, Superuser }; Actions = { Grant, Revoke, Open, Login,
Logout }; Resources = { Workstation, TIS, IDCertificate, IACertificate, PrivilegeCertificate,
AuthorizationCertificate } Any user can login to a workstation if the user has an
AuthorizationCertificate. Certificates are derived/enforced by the TIS based on the rules
highlighted above. A superuser can grant/revoke any certificate and logout any user.
Deliverable:
A UML model that establishes an appropriate RBAC policy according to the SecureUML
methodology. It is sufficient to submit a UML class diagrams (incl. dialect design), but not
required to design an UML profile. Submit a report displaying your class diagrams along with a
rationale for your design, no more than one side A4.
Indicative marking guideline: System, RBAC and dialect UML design [18 Marks]; Rationale [7
Marks]. It is sufficient to capture SecureUML elements conceptually.
Part C Formal Modelling [25 marks]
The Dafny file tokeneer.dfy2 has the beginning of an abstract formal model of part of the
tokeneer system in Dafny. The model is not intended to be executable. Your task is to extend the
model by answering the questions below.
Aim:
Develop an extended model of the tokeneer certificates and tokens. You do not need to provide
data to test your model. The aim of the exercise is to expand and refine the model specification.
Approach:
Follow the guidelines given in the questions below to extend the model.
The model consists of some abstract datatype definitions, some functions, predicates and
methods, and some traits and classes. A trait in dafny is similar to an abstract class or interface in
java: dafny requires that a class can only extend a trait, it cannot extend another class. This means
that we use traits to define superclasses. See for example the trait Certificate which is extended
by the class IDCert.
The key difference between a trait and a class is that a trait does not have a constructor defined.
A class must have a constructor: however, as can be seen in the model, the constructor can be
unspecified in an abstract model.
Deliverable:
A revised Dafny model for the tokens and certificates part of the tokeneer system. Include the full
content of your Dafny file (as text, not as a screenshot image) in your report. You can format it as
follows (by copying and pasting the content of your .dfy file into your word document):
/*
Solution to CSC8204 Coursework Part C
*/
// basic types
type optional<T> = ts: set<T> | |ts| <= 1
type TIME = nat
Questions:
1) Clearance class. Find the definition of Clearance, which has a single field (cClass) represented
by the enumerated type CLEARANCE_CLASS. A newly created Clearance object will initially
have the value unmarked.
a) Add a postcondition (ensures) to the constructor to record this. [2 marks]
2 The model is available as tokeneer.dfy in the repository https://github.com/SteveR-Ncl/CSC8204-Dafny
A ghost function minClearance has been specified. It should return the minimum of two
Clearance objects, ie Clearance(a,b) will return a if the object a has a lower clearance than b.
“Lower” is implied by the ordering of the enumeration, ie unmarked < unclassified < restricted
etc.
b) Complete the definition of ghost function minClearance to return the minimum clearance
object as described above. Use c1.cClass to access the value of the cClass field in the
object c1. Hint: you will need to use a reads clause as described in the lecture.
[4 marks]
2) Admin Privilege. A user can have one of 4 privileges, as shown by the enumerated datatype
definition PRIVILEGE. Only the admin roles (guard, auditManager, securityOfficer) have any
admin operations available to them, as follows:
• A guard can use the overrideLock operation
• An auditManager can use the archiveLog operation
• A securityOfficer can use the updateData and shutdownOp operations
a) Modify your model to add a new enumerated datatype called ADMINOP, with values
representing the four operations above (overrideLock, etc) [2 marks]
b) Add a function with signature as follows:
function availableOps(p: PRIVILEGE): set<ADMINOP>
Provide a function body which returns the set of operations available to a user with
privilege level p. [8 marks]
3) Token Predicates. A token class is defined in the model. It has fields for the tokenID and up
to 4 certificates held on the token (ID Certificate, Privilege Certificate, I and A Certificate, and
(optionally) Authorisation Certificate. Each certificate has its own ID; the Privilege, I and A and
Authorisation Certificates also contain the ID of the token and the ID of the ID certificate. There
are 3 predicate functions to define in the token class: ValidToken(), TokenWithValidAuth(),
CurrentToken(TIME).
Complete the predicate functions using the following definitions:
• A Valid Token has Privilege and I and A certificates correctly cross-referencing the ID
Certificate and TokenID. It need not have a valid Authorisation certificate.
• A Token with a Valid Authorisation must have an Authorisation certificate, and must
have correct cross-reference to the token ID and ID certificate’s ID
• A Current Token is defined using input parameter now, representing the current time. A
current token is a Valid Token where all the certificates are current, ie the current time is
included in the validityPeriods for each of the id certificate, privilege certificate and I
and A certificates.
Hint: set notation may be helpful here. Use a in B to express that a is a member of set B,
and B * C to indicate intersection of sets B and C. [9 marks]
Part D [25 marks]
This question makes use of the Floyd-Hoare logic to analyse code samples and investigate
whether they can be formally verified, using the approach described in the lectures on Program
Verification.
Aim:
The question assesses skill and understanding in formal verification, weakest precondition
semantics and Floyd-Hoare logic.
Deliverable:
Provide your answers to all the questions in Part D of you submission document.
Questions
For each of the two code samples shown, use the weakest precondition approach to derive any
necessary precondition in order to prove that the code is partially correct with respect to the
specification. Sample 2 uses information derived from the tokeneer scenario.
Be sure to show each step in the derivation and indicate which proof rules have been used.
1) Sums method [10 marks]
method Sums(x: int, y: int) returns (m: int, n: int)
ensures m > n
{
var a: int;
m := x;
n := y;
a := 2 * m + n;
n := n - 1;
m := a;
}
2) UpdateAlarms method [15 marks]
datatype ALARM = silent | alarming
method UpdateAlarms(doorAlarm: ALARM, auditAlarm: ALARM) returns (alarm: ALARM)
ensures (alarm == alarming) <==>
(doorAlarm == alarming) || (auditAlarm == alarming)
{
if doorAlarm == alarming || auditAlarm == alarming
{ alarm := alarming; }
else
{ alarm := silent ;}
}