*Answer all questions.*

*Time allowed: 2 hours*

*Total number of points: 100*

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,gc)C(J,gc)

C(assume(c),g) =gc

C(x=e,g) =gx=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,gc)P(J,gc)

P(assert(c),g) =gc

P(anything else,g) = true

Alpha assembly code:

op::= (Operand)

n(Integer Constant)

r(Register)_{i}

instr::= (Instruction)

ADDQr,_{s}op,r(Put_{d}r+_{s}opinr)_{d}

...

LDQr_{d}n(r) (Load from address_{s}r+_{s}n)

STQr_{s}n(r) (Store to address_{d}r+_{d}n)

RET (Return)

Operations on stores:

ρ [r_{i}n]

(Update store ρ soris_{i}n)

sel(r_{m},a)

(Select contents of memory addressa)

upd(r_{m},a,r)_{s}

(Update memory addressato contain contents ofr)_{s}

Machine model consists of steps:

(ρ_{1},pc_{1}) (ρ_{2},pc_{2})

1. If instruction *pc* is ADDQ *r _{s}*,

(ρ,pc) (ρ[r(_{d}r+_{s}op) ],pc+ 1)

2. If instruction *pc* is LDQ *r _{d}*

(ρ,pc) (ρ[rsel(_{d}r_{m},n+r) ],_{s}pc+ 1)

as long asrd(n+r)_{s}

3. If instruction *pc* is STQ *r _{s}*

(ρ,pc) (ρ[rupd(_{m}r_{m},n+r,_{d}r) ],_{s}pc+ 1)

as long aswr(n+r)_{d}

Safety predicate *SP* is defined:

PreVC_{0}

1. If instruction *pc* is ADDQ *r _{s}*,

VC=_{pc}VC[_{pc+1}r(_{d}r+_{s}op) ]

2. If instruction *pc* is LDQ *r _{d}*

VC= rd(_{pc}n+r)_{s}VC[_{pc+1}rsel(_{d}r_{m},n+r) ]_{s}

3. If instruction *pc* is STQ *r _{s}*

VC= wr(_{pc}n+r)_{d}VC[_{pc+1}rupd(_{m}r_{m},n+r,_{d}r) ]_{s}

4. If instruction *pc* is RET then:

VC=_{pc}Post

Commands:

c,d::=

x=e;

cd

if (e) {c} else {d}

while (e) {c}

Expressions:

e,f::=

x

n

e+f

e==f

...

Operations on memories:

μ(e)

(Evaluate expressionein memory μ)

μ [x:=n]

(Update memory μ soxisn)

Model of commands (*c*_{1}, μ_{1}) (*c*_{2}, μ_{2}):

1. If (*c*_{1}, μ_{1}) μ_{2}
then (*c*_{1}*d*, μ_{1}) (*d*, μ_{2})

2. If (*c*_{1}, μ_{1}) (*c*_{2}, μ_{2})
then (*c*_{1}*d*, μ_{1}) (*c*_{2}*d*, μ_{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 (*c*_{1}, μ_{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.

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.

Convert the following boolean expression into a BDD:

y( (xz) (zy) )

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

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

b) Rename all variables to be unique.

(Remember this may introduce phi-functions.)

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

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

b) Calculate *VC*_{1}, assuming *Post* = true.

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

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.

a) What was your favourite topic in this class?

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

You can use this sheet as scrap paper.

You can use this sheet as scrap paper.

You can use this sheet as scrap paper.

You can use this sheet as scrap paper.