PRACTICE FINAL SAMPLE SOLUTION
Note that for many of the questions, there's more than one right answer,
this is just one solution!
Question 1 (15 points)
a) What is a buffer overflow attack?
ANSWER:
A program running with rights P accepts input from a user with rights U;
the program expects a fixed-length input, and does not perform input
validation. The input is written into a fixed-length buffer, which
then overflows, writing the data into the adjacent area of memory.
The attacker uses this to write machine code into the area of memory,
and overwrites the saved program counter to cause the code to be
executed. The user is now running arbitrary code with rights P
rather than rights U.
b) What is rights escalation?
ANSWER:
We assign rights (such as read/write access to storage, ability to
execute programs...) to roles (such as users, administrators, network
services...). Rights escalation is when a role abuses a right they
have been granted to escalate their rights to include rights they have
not been granted.
c) Give an example of how a buffer overflow can lead to rights escalation.
ANSWER:
Role "anonymous" may be given the right to send http requests to port 80,
which in turn might execute a program which suffers from buffer overflow.
The buffer overflow causes arbitrary code to be executed with the rights
of the web server, which was not a right the anonymous user was granted.
d) Give two strategies for avoiding buffer overflows.
ANSWER:
Dynamic (i.e. run-time) checking of array bounds.
Static (i.e. compile-time) checking to ensure array bounds are never violated.
e) Compare the two strategies in your answer to (d): give an advantage and a disadvantage of each.
ANSWER:
Dynamic checks have a run-time penalty.
Static checks can only be an approximation (since checking for array
bounds violations is undecidable).
Question 2 (10 points)
Convert the following boolean expression into a BDD:
y => ( ( x xor z ) or ( z => !y ) )
You should assume the variable order x < y < z.
ANSWER:
x
/ \
F T
| \
| y
| / \
\ F T
\ | \
\ | z
\| / \
\ F T
\ / |
1 0
Gotten by computing the following decision tree:
x
/ \
/ \
/ \
/ \
/ \
y y
/ \ / \
/ \ / \
z z z z
/ \ / \ / \ / \
1 1 1 1 1 1 1 0
and then collapsing duplicate nodes, and replacing any nodes of the form:
x
/ \
| |
\ /
y
/ \
by:
x
/ \
Question 3 (30 points)
Consider the following function:
void foo (int x, int y) {
int z=0;
while (x > 0) {
z += y; x--;
}
assert (z == x*y);
}
Show the results of running the CBMC algorithm on this program.
a) Unwind function calls, loops and goto: just left with if and assignment.
ANSWER:
void foo (int x, int y) {
int z=0;
if (x > 0) { z = z+y; x = x-1; }
if (x > 0) { z = z+y; x = x-1; }
if (x > 0) { z = z+y; x = x-1; }
if (x > 0) { assume(false); }
assert (z == x*y);
}
(You can assume unwinding 3, and no unwinding assertions.)
b) Rename all variables to be unique.
(Remember this may introduce phi-functions.)
ANSWER:
void foo (int x0, int y0) {
int z0,...,z6; int x1,...,x6; int; z0 = 0;
if (x0 > 0) { z1 = z0+y0; x1 = x0-1; }
x2 = (x0 > 0? x1: x0); z2 = (x0 > 0? z1: z0);
if (x2 > 0) { z3 = z2+y0; x3 = x2-1; }
x4 = (x2 > 0? x3: x2); z4 = (x2 > 0? z3: z2);
if (x4 > 0) { z5 = z4+y0; x5 = x4-1; }
x6 = (x4 > 0? x5: x4); z6 = (x4 > 0? z5: z4);
if (x6 > 0) { assume(false); }
assert (z6 == x6*y0);
}
c) Calculate the constraints of the program C, and the properties of the program P.
Constraints:
ANSWER:
z0 = 0;
x0 > 0 => z1 = z0+y0; x0 > 0 => x1 = x0-1;
x2 = (x0 > 0? x1: x0); z2 = (x0 > 0? z1: z0);
x2 > 0 => z3 = z2+y0; x2 > 0 => x3 = x2-1;
x4 = (x2 > 0? x3: x2); z4 = (x2 > 0? z3: z2);
x4 > 0 => z5 = z4+y0; x4 > 0 => x5 = x4-1;
x6 = (x4 > 0? x5: x4); z6 = (x4 > 0? z5: z4);
x6 > 0 =>false;
Properties:
z6 == x6*y0;
NOTE: This program does not satisfy this property! (The bug is that
z6 == x0*y0, but z6 != x6*y0, that is x in the original program is now
zero, and that z == "original x" * y not z == "current x" * y.)
Question 4 (15 points)
Consider the following Alpha assembly program:
1. ADDQ r1, 8, r1
2. LDQ r2, 0(r1)
3. ADDQ r2, 5, r3
4. ADDQ r1, -8, r1
5. STQ r3, 0(r1)
6. RET
a) Show the steps of this program starting in state (1, rho) where rho is:
( r1 = 8, r2 = 4, r3 = 7, rm = { 1, 2, 3, 4 } )
ANSWER:
(1, ( r1 = 8, r2 = 4, r3 = 7, rm = { 1, 2, 3, 4 } ))
--> (2, ( r1 = 16, r2 = 4, r3 = 7, rm = { 1, 2, 3, 4 } ))
--> (3, ( r1 = 16, r2 = 3, r3 = 7, rm = { 1, 2, 3, 4 } ))
[ as long as rd(16) ]
--> (4, ( r1 = 16, r2 = 3, r3 = 8, rm = { 1, 2, 3, 4 } ))
--> (5, ( r1 = 8, r2 = 3, r3 = 8, rm = { 1, 2, 3, 4 } ))
--> (6, ( r1 = 8, r2 = 3, r3 = 8, rm = { 1, 8, 3, 4 } ))
[ as long as wr(8) ]
b) Calculate VC1, assuming Post = true.
ANSWER:
VC6 = true
VC5 = wr(r1) /\ VC6[ rm <- upd (rm, r1, r3) ]
= wr(r1) /\ true
VC4 = VC5[ r1 <- r1 + -8 ]
= wr(r1 + -8) /\ true
VC3 = VC4[ r3 <- r2 + 5 ]
= wr(r1 + -8) /\ true
VC2 = rd(r1) /\ VC3[ r2 <- sel(rm, r1) ]
= rd(r1) /\ wr(r1 + -8) /\ true
VC1 = VC2[ r1 <- r1 + 8 ]
= rd(r1 + 8) /\ wr(r1 + 8 + -8) /\ true
tidy up:
VC1 = rd(r1 + 8) /\ wr(r1)
Question 5 (15 points)
For each of these programs, say whether the program satisfies
sequential noninterference or not, and say whether it passes the
static analysis for noninterference or not. In each case, give a short
(one- or two-sentence justification for your answer).
a) xH = 1;
ANSWER: Noninterference yes. Static analysis yes.
No overt channels, no covert channels (since there's no control flow).
b) xH = yL;
ANSWER: Noninterference yes. Static analysis yes.
No overt channels, no covert channels (since there's no control flow).
Write up is fine, write down is the problem.
c) yL = xH;
ANSWER: Noninterference no. Static analysis no.
This suffers from an overt channel, with write down.
d) if (yL) { xH = 1; }
ANSWER: Noninterference yes. Static analysis yes.
No overt channels, no covert channels (since the if has no high variables in the condition).
e) if (xH) { yL = 1; }
ANSWER: Noninterference no. Static analysis no.
This suffers from a covert channels (since the if has a high variables
in the condition, and assigns to a low variable in the true branch).
f) xL = xL + yH; xL = xL - yH;
ANSWER: Noninterference yes. Static analysis no.
The static analyzer rejects this program, due to the overt flow xL =
xL + yH, but in fact no matter what the value of yH, the value of xL
afterwards is always the same as it was initially, so the program does
satisfy noninterference.
Question 6 (10 points)
Give an example of a covert timing channel, and describe (in English)
how it can be used to let one bit of information flow from a high
security variable to a low security variable.
ANSWER:
long timeL = System.getTimeMillis ();
while (xH && System.getTimeMillis () < timeL + 1000) { }
yL = (System.getTimeMillis () >= timeL + 1000);
If xH is true, then the while loop will run for at least 1000ms, and so
after the while loop terminates, yL will be true.
If xH is false, then the while loop will terminate immediately, and so
after the while loop terminates, yL will be almost certainly be false
(in theory, the program could be swapped out by the OS for 1000ms,
but this is quite unlikely).
As a result, this program copies the boolean variable xH into the boolean
variable yL.
Question 7 (5 points)
a) What was your favourite topic in this class?
ANSWER: Your call.
b) What was your least favourite topic in this class?
ANSWER: Your call, I think I'd go for "Trying to get cbmc to run under Windows." :-)