CSC8204 High Integrity Software Development - Secure Software Development Coursework 2023: Risk analysis, SecureUML design, formal modelling and verification
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:
-
Business goals of Praxis High Integrity Systems in undertaking the Tokeneer project. Rank the business goals according to the NIST business goal classification.
-
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.
-
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.
-
-
Conduct a risk synthesis connecting business goals, business risks and technical risks.
-
Derive one mitigation approach for each technical risk. Justify your choice.
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 V erification.
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 ;} }
