Name:

SE547 final exam: Practice exam

Time allowed: 2 hours

Total number of points: 100

CBMC Algorithm

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

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