Secure Software Development Coursework
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.
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 report[1] 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”.
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:
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 .
Evaluate:
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 . 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.dfy[2] 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]
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]
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]
Complete the predicate functions using the following definitions:
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 ;}
}
[1] Available from AdaCore at http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf
[2] The model is available as tokeneer.dfy in the repository https://github.com/SteveR-Ncl/CSC8204-Dafny
https://apaxresearchers.com/storage/files/2023/12/16/9667-YOZ_11_32_07_coursework20213pdf.docx
Not answered yet.
Copyright © 2012 - 2024 Apaxresearchers - All Rights Reserved.