1. Homepage
  2. Programming
  3. CSC8204 High Integrity Software Development - Secure Software Development Coursework 2023: Risk analysis, SecureUML design, formal modelling and verification

CSC8204 High Integrity Software Development - Secure Software Development Coursework 2023: Risk analysis, SecureUML design, formal modelling and verification

Engage in a Conversation
NewcastleNCLCSC8204High Integrity Software DevelopmentSecure Software DevelopmentRisk analysis SecureUML design formal modelling

CSC8204 CourseNana.COM

Secure Software Development CourseNana.COM

Coursework 2023 CourseNana.COM

Aims: CourseNana.COM

The aim of this assignment is to increase and assess understanding and resolution of risk analysis, SecureUML design, formal modelling and verification. CourseNana.COM

The coursework consists of 4 equally weighted questions. CourseNana.COM

Submission details:
Submission deadline: 15 Dec 2023, 15:30 CourseNana.COM

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. CourseNana.COM

The coursework is marked out of 100, with 25 marks for each question .
Support: CourseNana.COM

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. CourseNana.COM

Questions can also be posted in the Canvas discussion board. CourseNana.COM

Scenario: CourseNana.COM

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. CourseNana.COM

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”. CourseNana.COM

1 Available from AdaCore at http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf CourseNana.COM

Figure 1 Tokeneer system overview CourseNana.COM

The Tokeneer system displayed in Figure 1 consists of the secure enclave plus other components that are physically either inside or outside the enclave: CourseNana.COM

  • 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. CourseNana.COM

  • 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. CourseNana.COM

  • 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. CourseNana.COM

Part A Applied Risk Analysis [25 Marks] CourseNana.COM

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. CourseNana.COM

Aim: CourseNana.COM

Develop an applied risk analysis based on the documentation of the Tokeneer project (http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf). CourseNana.COM

Approach: CourseNana.COM

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. CourseNana.COM

Evaluate: CourseNana.COM

  1. Business goals of Praxis High Integrity Systems in undertaking the Tokeneer project. Rank the business goals according to the NIST business goal classification. CourseNana.COM

  2. Three main business risks affecting Praxis High Integrity Systems, including: Business risk indicator
    NIST business risk likelihood scaling
    NIST business risk impact scaling CourseNana.COM

    Overall NIST severity ranking. CourseNana.COM

    A one-sentence rationale, why you have chosen this risk over others. CourseNana.COM

  3. Five main technical risks determinable from the Tokeneer report and software CourseNana.COM

    deliverable. CourseNana.COM

    • Analyze the software artifacts CourseNana.COM

    • Evaluate the software security touchpoints CourseNana.COM

    • Use the 10 best practice security principles by McGraw. CourseNana.COM

    • Specify the risk likelihood and possible impact vis-à-vis of available controls. CourseNana.COM

    • Write a one-sentence rationale, why you have chosen this risk over others. CourseNana.COM

  4. Conduct a risk synthesis connecting business goals, business risks and technical risks. CourseNana.COM

  5. Derive one mitigation approach for each technical risk. Justify your choice. CourseNana.COM

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). CourseNana.COM

Aim: CourseNana.COM

Develop a high-level UML model in the style of SecureUML which models a suitable security policy for the Tokeneer ID station. CourseNana.COM

Figure 2 SecureUML Metamodel CourseNana.COM

Approach: CourseNana.COM

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). CourseNana.COM

Design: CourseNana.COM

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. CourseNana.COM

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. CourseNana.COM

Deliverable: CourseNana.COM

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. CourseNana.COM

Indicative marking guideline: System, RBAC and dialect UML design [18 Marks]; Rationale [7 Marks]. It is sufficient to capture SecureUML elements conceptually. CourseNana.COM

Part C Formal Modelling [25 marks] CourseNana.COM

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. CourseNana.COM

Develop an extended model of the tokeneer certificates and tokens. You do not need to provide CourseNana.COM

data to test your model. The aim of the exercise is to expand and refine the model specification. CourseNana.COM

Approach: CourseNana.COM

Follow the guidelines given in the questions below to extend the model. CourseNana.COM

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. CourseNana.COM

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. CourseNana.COM

Deliverable: CourseNana.COM

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): CourseNana.COM

Solution to CSC8204 Coursework Part C

 // basic types

type optional<T> = ts: set<T> | |ts| <= 1 type TIME = nat CourseNana.COM

Questions: CourseNana.COM

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. CourseNana.COM

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 CourseNana.COM

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. CourseNana.COM

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. CourseNana.COM

[4 marks] CourseNana.COM

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: CourseNana.COM

  1. a)  Modify your model to add a new enumerated datatype called ADMINOP, with values representing the four operations above (overrideLock, etc) [2 marks] CourseNana.COM

  2. 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] CourseNana.COM

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). CourseNana.COM

Complete the predicate functions using the following definitions: CourseNana.COM

  • 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. CourseNana.COM

  • 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 CourseNana.COM

  • 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. CourseNana.COM

    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] CourseNana.COM


Part D [25 marks] CourseNana.COM

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. CourseNana.COM

Aim: CourseNana.COM

The question assesses skill and understanding in formal verification, weakest precondition semantics and Floyd-Hoare logic. CourseNana.COM

Deliverable: CourseNana.COM

Provide your answers to all the questions in Part D of you submission document. CourseNana.COM

Questions CourseNana.COM

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. CourseNana.COM

Be sure to show each step in the derivation and indicate which proof rules have been used. CourseNana.COM

1) Sums method [10 marks] CourseNana.COM

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; } CourseNana.COM

2) UpdateAlarms method [15 marks] CourseNana.COM

datatype ALARM = silent | alarming CourseNana.COM

method UpdateAlarms(doorAlarm: ALARM, auditAlarm: ALARM) returns (alarm: ALARM) ensures (alarm == alarming) <==> CourseNana.COM

(doorAlarm == alarming) || (auditAlarm == alarming) CourseNana.COM

if doorAlarm == alarming || auditAlarm == alarming CourseNana.COM

{ alarm := alarming; } CourseNana.COM

else CourseNana.COM

{ alarm := silent ;} }  CourseNana.COM

Get in Touch with Our Experts

Wechat WeChat
Whatsapp Whatsapp
Newcastle代写,NCL代写,CSC8204代写,High Integrity Software Development代写,Secure Software Development代写,Risk analysis代写, SecureUML design代写, formal modelling代写,Newcastle代编,NCL代编,CSC8204代编,High Integrity Software Development代编,Secure Software Development代编,Risk analysis代编, SecureUML design代编, formal modelling代编,Newcastle代考,NCL代考,CSC8204代考,High Integrity Software Development代考,Secure Software Development代考,Risk analysis代考, SecureUML design代考, formal modelling代考,Newcastlehelp,NCLhelp,CSC8204help,High Integrity Software Developmenthelp,Secure Software Developmenthelp,Risk analysishelp, SecureUML designhelp, formal modellinghelp,Newcastle作业代写,NCL作业代写,CSC8204作业代写,High Integrity Software Development作业代写,Secure Software Development作业代写,Risk analysis作业代写, SecureUML design作业代写, formal modelling作业代写,Newcastle编程代写,NCL编程代写,CSC8204编程代写,High Integrity Software Development编程代写,Secure Software Development编程代写,Risk analysis编程代写, SecureUML design编程代写, formal modelling编程代写,Newcastleprogramming help,NCLprogramming help,CSC8204programming help,High Integrity Software Developmentprogramming help,Secure Software Developmentprogramming help,Risk analysisprogramming help, SecureUML designprogramming help, formal modellingprogramming help,Newcastleassignment help,NCLassignment help,CSC8204assignment help,High Integrity Software Developmentassignment help,Secure Software Developmentassignment help,Risk analysisassignment help, SecureUML designassignment help, formal modellingassignment help,Newcastlesolution,NCLsolution,CSC8204solution,High Integrity Software Developmentsolution,Secure Software Developmentsolution,Risk analysissolution, SecureUML designsolution, formal modellingsolution,