# Name:

SE547 final exam: Practice exam

Time allowed: 2 hours

Total number of points: 100

### CBMC Algorithm

1. Start with a C program with assert(...) and assume(...) statements.

2. Preprocess the program: just left with functions, loops, if, goto and assignment.

3. Unwind function calls, loops and goto: just left with if and assignment.

4. Rename all variables to be unique.

5. Calculate the constraints of the program C, and the properties of the program P.

6. Verify C P using a SAT-solver.

For a program I, the constraints are C(I,true) where C(I,g) is defined:

C(I;J, g) = C(I, g) C(I, g)
C(if (c) { I } else { J }, g) = C(I, g c) C(J, g c)
C(assume(c), g) = g c
C(x=e, g) = g x=e
C(anything else, g) = true

For a program I, the properties are P(I,true) where P(I,g) is defined:

P(I;J, g) = P(I, g) P(I, g)
P(if (c) { I } else { J }, g) = P(I, g c) P(J, g c)
P(assert(c), g) = g c
P(anything else, g) = true

### Proof Carrying Code reference

Alpha assembly code:

op ::=    (Operand)
n    (Integer Constant)
ri    (Register)

instr ::=    (Instruction)
ADDQ rs, op, rd    (Put rs + op in rd)
...
LDQ rd n(rs)    (Load from address rs + n)
STQ rs n(rd)    (Store to address rd + n)
RET    (Return)

Operations on stores:

ρ [ ri n ]
(Update store ρ so ri is n)
sel(rm, a)
(Select contents of memory address a)
upd(rm, a, rs)
(Update memory address a to contain contents of rs)

### Proof Carrying Code reference

Machine model consists of steps:

1, pc1) 2, pc2)

1. If instruction pc is ADDQ rs, op, rd then:

(ρ, pc) (ρ[ rd (rs + op) ], pc + 1)

2. If instruction pc is LDQ rd n(rs) then:

(ρ, pc) (ρ[ rd sel(rm, n + rs) ], pc + 1)
as long as rd(n + rs)

3. If instruction pc is STQ rs n(rd) then:

(ρ, pc) (ρ[ rm upd(rm, n + rd, rs) ], pc + 1)
as long as wr(n + rd)

Safety predicate SP is defined:

Pre VC0

1. If instruction pc is ADDQ rs, op, rd then:

VCpc = VCpc+1 [ rd (rs + op) ]

2. If instruction pc is LDQ rd n(rs) then:

VCpc = rd(n + rs) VCpc+1[ rd sel(rm, n + rs) ]

3. If instruction pc is STQ rs n(rd) then:

VCpc = wr(n + rd) VCpc+1[ rm upd(rm, n + rd, rs) ]

4. If instruction pc is RET then:

VCpc = Post

### Noninterference reference

Commands:

c, d ::=
x = e;
c d
if (e) { c } else { d }
while (e) { c }

Expressions:

e, f ::=
x
n
e + f
e == f
...

Operations on memories:

μ(e)
(Evaluate expression e in memory μ)
μ [ x := n ]
(Update memory μ so x is n)

Model of commands (c1, μ1) (c2, μ2):

1. If (c1, μ1) μ2 then (c1d, μ1) (d, μ2)

2. If (c1, μ1) (c2, μ2) then (c1d, μ1) (c2d, μ2)

3. If μ(e) is nonzero then (if (e) {c} else {d}, μ) (c, μ)

4. If μ(e) is zero then (if (e) {c} else {d}, μ) (d, μ)

5. If μ(e) is nonzero then (while (e) {c}, μ) (c while (e) {c}, μ)

Model of commands final step (c1, μ1) μ2:

6. (x=e, μ) μ[x:=μ(e)]

7. If μ(e) is zero then (while (e) {c}, μ) μ

Write μ ~ ρ whenever μ and ρ agree on L variables.

A command c satisfies sequential noninterference when:

If μ1 ~ ρ1 and (c, μ1) * μ2 and (c, ρ1) * ρ2 then μ2 ~ ρ2.

Static analysis for noninterference satisfying:

1. In x = e, if e reads from an H variable, then x is an H variable.

2. In if (e) { c } else { d }, if e reads from an H variable, then c and d only write to H variables.

3. In while (e) { c }, if e reads from an H variable, then c only writes to H variables.

### Question 1 (15 points)

a) What is a buffer overflow attack?

b) What is rights escalation?

c) Give an example of how a buffer overflow can lead to rights escalation.

d) Give two strategies for avoiding buffer overflows.

e) Compare the two strategies in your answer to (d): give an advantage and a disadvantage of each.

### Question 2 (10 points)

Convert the following boolean expression into a BDD:

y ( ( x z ) ( z y ) )

You should assume the variable order x < y < z.

### 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.

(You can assume unwinding 3, and no unwinding assertions.)

### Question 3 continued

b) Rename all variables to be unique.

(Remember this may introduce phi-functions.)

### Question 3 continued

c) Calculate the constraints of the program C, and the properties of the program P.

### 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, ρ) where ρ is:

( r1 = 8, r2 = 4, r3 = 7, rm = { 1, 2, 3, 4 } )

### Question 4 continued

b) Calculate VC1, assuming Post = true.

### 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;

b) xH = yL;

c) yL = xH;

d) if (yL) { xH = 1; }

e) if (xH) { yL = 1; }

f) xL = xL + yH; xL = xL - yH;

### 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.

### Question 7 (5 points)

a) What was your favourite topic in this class?

b) What was your least favourite topic in this class?

### Worksheet

You can use this sheet as scrap paper.

### Worksheet

You can use this sheet as scrap paper.

### Worksheet

You can use this sheet as scrap paper.

### Worksheet

You can use this sheet as scrap paper.