Overview

Software Security

Software Model Checking

Logical Satisfaction

Binary Decision Diagrams

Implementing BDDs

Secure software is intended to grant *rights*
to users acting in certain *roles*.

What are examples of rights and roles?

Incorrect software can result in *rights escalation*.
What is this? What are examples?

What are common strategies for attackers achieving rights escalation?

What can we do about these attacks?

What is a buffer overflow attack?

Can buffer overflow attacks occur in C? In Java?

What language feature of C or Java allows buffer overflows?

What can we do about it? Statically? Dynamically?

What are the tradeoffs between static and dynamic checks?

What is a software model checker?

How does a software model checker compare to conventional testing?

Can a software model checker find all bugs?

Software model checkers translate source code into (possibly big!) logical formulas. For example:

void foo (int x, int y) { char[] z = new char[x+1]; if (y < x) { z[y] = 'a'; } }

Is this program safe? What logical formula do we generate from it?

We have turned the problem of software model checking into the problem of logical satisfaction.

More on software model checkers later...

What is first order predicate logic? What is logical satisfaction?

Logical satisfaction is NP-complete. What does this mean? What is the best-known running time for an NP-complete problem?

For example, how long will it take to determine satisfaction for:

x: uint16 .y: uint16 .z: uint16 . (x+y) +z=x+ (y+z)

Try it... simplebdd.zip
contains a `TestArithBrute`

class.

Logical satisfaction is solved by SAT-solvers.

High-quality production SAT-solvers exist Chaff, zChaff, ... See satlive.org.

We have success stories of using zChaff to solve problems with more than one million variables and 10 million clauses.

--zChaff web site

A common simple solution is *binary decision diagrams*.

Try it... simplebdd.zip
contains a BDD-based `TestArith`

class.

A first shot at solving satisfaction: convert to Disjunctive Normal Form (DNF).

What is DNF?

How do we check satisfiability of a formula in DNF?

Why is this not an acceptable solution?

A better shot; use:

st,uread as `ifsthentelseu'

Convert to If-then-else Normal Form (INF).

What is INF?

What is the INF for the following:

xyz

We can draw INFs as *binary decision trees*.
What is a decision tree? What is the decision tree
for this formula?

Decision trees are still not acceptable: why not?

A decision *diagram* is a decision tree where
we *share* nodes.

What is the decision diagram for the following:

xyz

What is the decision diagram for the follwing:

x_{1}...x_{n}

Hooray, much better!

Binary Decision Diagrams are a graphical representation of the grammar:

s,t,u::=

0

1

xt,u

A couple of improvements to Binary Decision Diagrams:

a) What should we do about
*x*
*t*,
*t*? [*Reduced* BDDs.]

b) There are two representations of
*x*
*y*: what are they? What should we do about this? [*Ordered* BDDs.]

Reduced, Ordered BDDs have the following very nice property:

tuis a tautology just whent=u

that is *syntactic equality* is the same as *semantic equality*.

In particular, for ROBDDs:

- The only tautology is 1.
- The only unsatisfiable formula is 0.

This makes checking for satisfiability pretty easy! (But remember that satisfiability is NP-complete; where did the hard work go?)

How can we convert this grammar into a class hierarchy?

s,t,u::=

0

1

xt,u

Hint: start with:

interface BoolPred { BoolPred ite (BoolPred p, BoolPred q); // this -> p, q ... static final BoolPred T = ...; static final BoolPred F = ...; }

How can we implement the ite method?

interface BoolPred { BoolPred ite (BoolPred p, BoolPred q); // this -> p, q ... static final BoolPred T = ...; static final BoolPred F = ...; }

Implementation trick: *use the flyweight pattern*. What is this?
Why does it help?

(Other names for this kind of flyweighting: dynamic programming, memoization...)

A very simple implementation of BDDs is in `simplebdd.bool.BoolPred`

in simplebdd.zip (approx. 150loc!).

BDDs are just about binary data, but we can code up fixed-width arithmetic...

How do we code an *n*-bit integer variable?

How do we code an *n*-bit integer expression?

How do we code *n*-bit integer arithmetic?

A partial implementation is in `simplebdd.integer.IntPred`

in simplebdd.zip (approx. 200loc).

Model checking.