代写CSC8204R SECURE SOFTWARE DEVELOPMENT 2024

CSC8204R

SECURE

SOFTWARE DEVELOPMENT

MAY 2024

Question 1 (35 marks)

This question focuses on information flow control and non- interference. Your task is to develop a programme semantics computation tree. The scenario is a chemical plant in which parameters for efficiency of the chemical reaction are secret. The secrets are activation energy, expressed as target temperature T* = 1200, and target acidity A * = 3.18. The variables T and A carry current measurements of temperature and acidity, which can be observed by the adversary before the chemical reaction.

The variables buffer B and heater H are public. Consider the following programme:

B := 0; H := 0;

print(A, T);

if A <> A* then B := (A-A*)*10;

if T < T* then H := T*-T;

if (B <> 0 OR H > 0) then print(B, H);

a)   Construct the initial programme state for the programme. [5 Marks]

b)   Construct a computation tree for the programme execution [20 Marks]

c)   Identify under which circumstances an adversary can determine the values for the secrets target temperature T* and target acidity A*. How are the secrets computed?   [10 marks]

Question 2 (15 marks)

This question considers role-based access control for the scenario of an industrial control system of a chemical pipeline. We are using model-based architecture and SecureUML as implementation tools, based on the UML framework below.

For each of the following questions provide a fragment of UML and realizes the desired design.

a)   Design role classes for an Engineer and an Administrator role, in which Administrators gain all permissions of Engineers.           [2 marks]

b)   The pipeline has Station, Actuator (Valve and Pump), Sensor and Alarm resource classes. Model these resources including the resource derivation, in which a Station can have multiple Actuators, Sensors, and Alarms.       [3 marks]

c)   Model the atomic actions Read, Activate, and Deactivate. Establish a composite action Shutdown, which can incorporate multiple Deactivate actions.                  [5 marks]

d)   How would you model that only an Administrator role can execute the Shutdown action on Stations? How do you model that,  if an Alarm is active, all users can initiate a Shutdown.                                        [5 marks]

Question 3 (35 marks)

This question is based on a scenario of a chemical plant, in which experts with given qualifications are expected to be able to deal with alarms that are raised.

Write a model in Dafny to represent the following information:

1. There are 4 kinds of alarm that could be raised: these are Electrical, Mechanical, Biological, Chemical. Represent these using an enumerated datatype called QUALIFICATION.    [5 marks]

2.  An Alarm is modelled as a class with 2 variables. One represents the qualification of the alarm, the other is a description of the alarm represented as a string.           [5 marks]

3. An Expert has several qualifications. Model this as a class with a variable to represent the set of qualifications held by the expert. Include in your class definition a predicate function called Valid(), which returns true if and only if the set of qualifications is not empty. Hint: remember to use a reads clause to ensure visibility of class variables.                                                         [10 marks]

4.  The plant is modelled by a class that has a variable to represent a set of alarms and a variable to represent a set of experts. For consistency of the whole plant, it is necessary that each type of alarm is covered by at least one expert. This means that for all alarms, there is an expert that includes the alarm’s qualification in their set of qualifications.

Write a class to represent the Plant and the sets of alarms and experts. Include in your class definition a predicate  function called Complete(), which returns true if and only if the alarms are covered by qualified experts as noted above.              [15 marks]

Question 4 (15 marks)

These questions in this section assess skill and understanding informal verification, weakest precondition semantics and Floyd- Hoare logic.

Use the process of postcondition hoisting to show how a verification condition is generated for the following code fragments, expressed as Hoare Triples. Be sure to show all steps in the derivation and refer to the rules used at each step.

a) {true} Y := 3 * X; { Y > 60 } [4 marks]

b) { X = Y } X := X – 1; Y := Y – 1; { X = Y }                       [5 marks]

c) {true} if C > M then M := C end if { M >= C }                   [6 marks]