Software Security
CSG 379/ Karl Lieberherr
============================================
Due date: October 4, 2004

The home directory of the course is:
http://www.ccs.neu.edu/home/lieber/courses/csg379/f04/

f04.html is the course home page.

Reading assignment: Read on the average 3 chapters per week from the text book.
In 6 weeks you should be done.

Part 1:
Exploring a Binder object using AspectJ
---------------------------------------

So far we have used AspectJ to implement security related
behavior. AspectJ is also useful for many other aspects
because it is a general purpose aspect-oriented language.

Analyze the Binder object m you created 
in the previous homework as follows:


Copy the code in 

/home/lieber/.www/courses/csg379/f04/hw/3/binder

and compile it with

compile

and run it with 

run

Follow the directions in:

/home/lieber/.www/courses/csg379/f04/daj/daj-directions

to set-up your CCIS environment and run the program.

The above link also tells you how to generate a parser 
yourself.

There are two tasks to do:

1. Find out how the program works and simulate its behavior
without using "declare strategy" and "declare traversal".
In other words, remove file Sample.trv and simulate the equivalent
using AspectJ.
Use intertype
declarations to add your own methods to the existing classes.
For an example, see file:
interType.java

Here are the files you need to understand:
Sample.trv
  Defines object navigation (WhereToGo).
Printer.java
  Defines WhenAndWhatToDo during navigation.
interType.java
  Adds methods to classes defined by program.cd.

The following files are from the previous homework:
Main.java
program.cd
program.input

2. Discuss the software security implications of the two solutions:
The declarative approach used in Sample.trv versus the manual 
approach.

What kind of security vulnerabilities could creep in with
the two appoaches? Which one is less prone to vulnerabilities?


Part 2: Limitations of AspectJ for statically checking security policies
------------------------------------------------------------------------

The declare construct of AspectJ is also useful for declaring
warnings:

declare warning: !pointcutExpression : 
  "violation of policy expressed by pointcutExpression";

This question is motivated by a paper by Ken Ashcraft and
Dawson Engler  on Using Programmer-Weitten Compiler Extensions
to Catch Security Holes (2002 IEEE Symposium on Security and
Privacy).

Part 2.A:
Which poincut primitives may appear in a declare warning statement?

Part 2.B:
Print a warning when a program reads from an untrustworthy source:

It calls a method Object copy_from_user() or Object get_user().

Part 2.C:
Check that data from an untrustworthy source is checked
with a method called plausibility_check(Object o).
Can you do this statically or only dynamically?

Part 2.D:
Propose one way to extend AspectJ to make it
more powerful for checking statically for vulnerabilities.


Part 3: The complexity of AspectJ pointcuts 
        Complexity Theory and Security
-------------------------------------------

When we write security policies in AspectJ, we need
to be aware of the computational complexity of our 
policies. There is a tradeoff between security and efficiency
and an application could be too inefficient because
of high security.
Consider a pointcut using call(), cflow(), || and &&.
We call this language SAJ-without-complement.

Consider a Java program that uses a pointcut in this language
and we ask the question: Will the pointcut select a join point
for at least one execution of the program.
Clearly, if it does not, the security policy 
expressed by the pointcut would be inconsistent.

We claim that if there would be a polynomial-time
algorithm for checking
whether such a pointcut is consistent,
then there would be a polynomial-time algorithm
for finding a satisfying assignment in
a boolean formula.

Your task is to prove this statement and to implement
an example of the reduction in AspectJ.

Here is a hint how to do the reduction:

Given is a boolean formula of the form
(+ is or, the lines are anded together)

x1 + !x2 + x3
x1! + x2
x1
           !x3

etc.

We construct a Java program as follows: the call
main() contains a call to X1.f() and Nx1.f().
X1.f() and Nx1.f() contain a call to X2.f() and Nx2.f().
X2.f() and Nx2.f() contain a call to X3.f() and Nx3.f().
X3.f() and Nx3.f() contain a call to Target.f().

Now we construct a pointcut for the first line as follows:

pointcut line1() :
  cflow(call (void X1.f())) || 
  cflow(call (void Nx2.f())) || 
  cflow(call (void X3.f())); 

For the remaining lines:

pointcut line2() :
  cflow(call (void Nx1.f())) || 
  cflow(call (void X2.f())); 
etc.

pointcut all :
  line1() && line2() && line3() && line4();

Part 3.A:
Prove that for the general form of this construction,
the boolean formula is satisfiable if
and only if the pointcut is consistent.

Part 3.B:
Write a complete AspectJ program that encodes the formula:
x1 + !x2 + x3
x1! + x2
x1
           !x3

and run the program on two inputs.

Then add

     !x2

to make the formula unsatisfiable.

Part 3.C:
Does AspectJ tell you that the pointcut will never succeed?
Should it?

Part 3.D:
Provide your own proof that if their is a polynomial-time
algorithm for pointcut implication, then there is a polynomial-time
algorithm for the satisfiability of boolean formulas.

Pointcut implication is defined as follows:
Give two pointcuts p1 and p2 and a program G,
for all executions of G the set of join points selected
by p1 is a subset of the join points selected by p2.

This part is motivated by

http://www.ccs.neu.edu/research/demeter/papers/unified/unified.pdf

where you can find more background information.

Turn in your AspectJ program, input, outputs and
your discussion.

===========================================

Where to turn in:

csg379-grader AT ccs.neu.edu

Questions to the same address: it reaches both Robbie and me.