Practice Exam
Started: May 31 at 0:50
Quiz Instructions
This is a practice exam, designed to have the same format and similar styles of questions to the final exam for SWEN90010 in Semester 1 2022.
Copyright By PowCoder代写 加微信 powcoder
You should use this exam to test your IT set up for the final exam and to get used to answering questions via the Canvas Quiz interface.
The final exam will also be delivered via Canvas Quiz. We recommend that you undertake the practice exam as if it were the final exam, i.e. under the same conditions and restrictions (see below) as will be in place for the final exam.
The following instructions apply to the final exam and will also be present on the final exam:
The final exam is an open book assessment.
While you are undertaking the final exam you are permitted to:
make use of the course notes and lecture slides (including soft-copy versions)
make use of the example programs that have been part of this subject, including any code that you have written, provided that you include suitable attribution
make use of the sample solutions to the assignments, provided you include suitable attribution
make use of tools such as Alloy, GNAT GPS, gnatmake, gnatprove, for checking, compiling, or executing Alloy models Ada programs respectively.
While you are undertaking the final exam you must not:
make use of any messaging or communications technology
make use of any world-wide web or internet-based resources such as wikipedia, stackoverflow, or google and other search services
act in any manner that could be regarded as providing assistance to another student who is undertaking the final exam, or will in the future be undertaking the final exam.
The work you submit must be based on your own knowledge and skills, without assistance from any other person.
Question 1 4 pts
A building’s automatic fire sprinkler system consists of a water sprinkler, installed into the building’s ceiling, as well as two smoke detectors, plus other components mentioned below. The purpose of the system is to automatically activate the sprinkler when a fire is detected by either of the smoke detectors.
Sprinklers and Pump When a fire is detected, the system activates a water pump, to feed water to the sprinkler. If the sprinkler’s nozzle is not blocked and the water pump is activated, water will flow from the sprinkler.
Smoke Detectors The system employs two smoke detectors to detect fires. Each is designed to act as a redundant back-up for the other: a fire is detected if either of the
detectors is triggered (that is, if either of the smoke detectors detects smoke).
Safety condition A hazard occurs when there is smoke but water does not flow from the sprinkler system.
Suppose you have been asked to perform a fault-tree analysis on this system, for this hazard.
The top-level event (i.e. the root) for the fault tree is the case in which there is smoke but water does not flow from the sprinkler system.
The following components in the system can each fail, and are assumed to fail independently of each other. These failures constitute the basic failure events (i.e. the leaves) of the fault tree:
The smoke detectors (each of which fails independently of the other) The water pump
The sprinkler nozzle (by becoming blocked)
For each of the fault-trees below, decide whether it is correct or incorrect for this scenario and hazard.
[ Select ]
[ Select ]
Fault Tree 1 is
Fault Tree 2 is
Fault Tree 3 is
[ Select ]
Fault Tree 4 is
[ Select ]
Question 2 2 pts
The minimum number of smoke detectors required so that the building’s automatic fire sprinkler system can mask smoke detector failures is . In this case, the
system will operate correctly in the presence of at most smoke detector failure(s).
Question 3 6 pts
For each STRIDE security threat, which security property does it correspond to?
Repudiation
Information Disclosure
Denial of Service
Elevation of Privilege
[ Choose ]
[ Choose ]
[ Choose ]
[ Choose ]
[ Choose ]
[ Choose ]
Question 4 2 pts
Consider a fictitious web based system that comprises the following four components: users, a web server, a third-party identity provider service, and a database back-end server.
Users access the system using their web browser
A web server receives the user requests and makes use of two other servers to process them
The web server communicates with a third-party identity provider service to authenticate users
The web server also communicates with a database back-end server to service each user request by fetching data from the database that the user is authorised to read
The web server and the database back-end are both controlled by the same organisation. However the third-party identity provider is not under the control of that organisation.
How many trust boundaries exist in this system? You may assume that all users reside in the
[ Select ]
same trust boundary.
Question 5 12 pts
For each of the STRIDE categories, for the system from the previous question, list 2 (two) threats from that category that are applicable for the system.
Edit View Insert Format Tools Table
12pt Paragraph
0 words
Question 6 1 pts
The following Alloy code models part of a file system, which stores a collection of files. A file contains data and also an access control list (ACL). A file’s ACL specifies which users are allowed to access the file and which permissions each user has to access the file. Here we consider just Read and Write permissions. A state of the system is mapping from filenames to files.
The following signature declarations model the state of the system described above.
sig Data {}
sig User {}
sig FileName {}
abstract sig Permission {}
one sig Read, Write extends Permission {}
sig File {
contents : Data ,
acl : User -> Permission
one sig State {
var files : FileName -> File
Write a fact declaration that specifies that the files mapping of every State is a function, i.e. that there is at most one file associated with each filename.
Edit View Insert Format Tools Table
12pt Paragraph
0 words
Question 7 2 pts
(Continuing the file system model from the previous question.)
Write a fun declaration (i.e. an Alloy function) called permissions that takes as its arguments a User u, FileName f and a State s and returns the set of permissions that u has to f in state s.
Edit View Insert Format Tools Table
12pt Paragraph
0 words
Question 8 7 pts
(Continuing the file system model from the previous question.)
Complete the definition of the following predicate that models the copy operation. The copy operation, executed on behalf of the user u, copies the contents of the source file whose name is src to the destination file whose name is dest. State s is the state before the copy operation.
If the destination file does not exist, the copy operation creates it and sets its access control list to new_acl[u] where the new_acl function is given below. Copy does not modify the ACL of an existing destination file.
If the destination file already exists, then copy can proceed only if user u has Write permission to the destination file; similarly copy can proceed only if u has Read permission to the source file.
fun new_acl[u : User] : (User -> Permission) {
(u -> Permission)
pred copy[u: User, src: FileName, dest: FileName, s: State] {
// complete this definition
Edit View Insert Format Tools Table
12pt Paragraph
0 words
Question 9 1 pts
(Continuing the file system model from the previous question.)
When copy creates a new file, explain in words which users are allowed to access that file and with what permissions?
Edit View Insert Format Tools Table
12pt Paragraph
p 0 words
Question 10 1 pts
(Continuing the file system model from the previous question.)
We can define when a state transition occurs on behalf of a user u as follows.
Explain in words the meaning of the following assertion: what is it trying to check about state transitions?
pred state_transition[u : User, s : State] {
some src : FileName, dest : FileName | copy[u,src,dest,s]
assert write_safe {
all u : User, s : State | state_transition[u,s] implies
(all f : FileName | Write not in permissions[u,f,s] implies
s.files'[f] = s.files[f])
Question 11 2 pts
(Continuing the file system model from the previous question.)
Should a correct copy operation, as defined above, satisfy this assertion? If so, explain why. If not, explain how the assertion should be changed so that a correct copy operation always satisfies it.
Question 12 4 pts
(Continuing the file system model from the previous question.)
Write an assertion read_safe that checks that the only files that can be read by a state transition are those to which the user has Read permission.
Question 13 2 pts
Consider the following snippet of C code that adds two signed integers and returns the result.
To understand this code, suppose we compile and run this code on a platform in which integers are 32-bits wide. Imagine that we call add with a = 2147483647 and b = 10. In this case, add returns −2147483639.
Translate this function directly into Ada, using the standard Integer type for signed integers. i.e. define an Ada implementation of this function that given two Integer arguments a and b, returns a+b, where “+” is the standard addition operator on Ada signed Integers.
int add(int a, int b){
return (a + b);
Question 14 1 pts
(Continuing the add Ada function from the previous question.)
If we compile and run an Ada version of this function, on a platform with 32-bit Integers, passing it the values of a = 2147483647 and b = 10, the program results in
a CONSTRAINT_ERROR being raised. Why does this error occur:
Integer underflow has occurred
Integer overflow has occurred
The result of a+b is larger than can fit into the 32-bit signed integer type Undefined behaviour has occurred
Question 15 3 pts
(Continuing the add Ada function from the previous question.)
Write a suitable precondition for your Ada implementation of the add function, to guarantee that it is free of errors. Your precondition should be no stronger than necessary (i.e. it should be the weakest precondition that ensures that the function is free of errors).
Question 16 2 pts
(Continuing the add Ada function from the previous question.)
Suppose you call your add function from some other piece of code, passing it the values of a = 2147483647 and b = 10. Would it satisfy your precondition? If so, explain why. If not, explain why not.
Question 17 3 pts
Consider the program below. This program searches the array A whose length is N and whose valid indexes are between 0 and N − 1 inclusive. For this question you can assume that N ≥ 0 always. The program searches for a value X in the array. If it finds X then the variable pos is set to the index of X in the array. Otherwise, if X is not in the array, the final value of pos should be -1. If pos’s final value is not -1, then pos must be a valid index, i.e. 0 ≤ pos ≤ N − 1.
pos := −1;
while i != N and pos = −1 do
if A[i] = X then
i := i + 1
We can express the correctness of this program via the Hoare triple: {true} S {Q} where S is the program above and the postcondition Q is defined as follows:
where the predicate notfound(k) states that the first k elements of the array A are not X:
Explain why this postcondition guarantees that when X is present in the array, then pos is guaranteed to be set to the index of X in the array.
Question 18 4 pts
(Continuing the Hoare logic example from the previous question.)
Write down a suitable loop invariant I for the while-loop of this program that is strong enough to guarantee the postcondition Q given above.
Question 19 8 pts
(Continuing the Hoare logic example from the previous questions.)
Use the rules of Hoare logic to prove that this program satisfies the Hoare logic statement {true} S {Q} where S is the program above and the postcondition Q is defined as above.
Note: you might like to use the equation editing features of Canvas to write your answer. (At the right end of the editing toolbar, press the 3 vertical dots and then select the button that has a square root symbol.) Alternatively, you can also write your answer as plain text using suitable notation. For instance, you could write “forall” instead of the “∀” symbol, etc. Use whatever style you find easiest, so long as your answer is clearly set out.
Question 20 3 pts
Consider the following Ada program.
procedure Pointers is
X : access Integer := new Integer'(5);
Y : access Integer := X;
Y.all := 10;
end Pointers;
Variable Y is called an [ Select ] for X because
[ Select ]
[ Select ]
. After this program finishes executing, the statement “X.all =
Saved at 0:52
Submit Quiz
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com