SE547: Lecture 1 (Security Automata)

Contents [0/20]

Overview: Topics (tentative) [1/20]
Overview: Class Audience [2/20]
Overview: Class Style [3/20]
Overview: Background [4/20]
Overview: Topics of Interest: Foundations [5/20]
Overview: Topics of Interest: Language Mechanisms [6/20]
Overview: Topics of Interest: Logic and Security [7/20]
Overview: Topics of Interest: Cryptographic Protocols [8/20]
Overview: Topics of Interest: Current Techniques [9/20]
Overview: Course Project [10/20]
Overview: Course Project: Milestones [11/20]
Overview: Example Project: Cryptographic programming in Jif [12/20]
Overview: Other Project Topics [13/20]
Overview: Your Job [14/20]
Intro [15/20]
Security Automata: [16/20]
Security Automata: Polymer [17/20]
Security Automata: Disallow Println [18/20]
Security Automata: Limit Open Files [19/20]
Security Automata: [20/20]

Overview: Topics (tentative) [1/20]

Overview: Class Audience [2/20]

Foundations of Computer Security is for

Overview: Class Style [3/20]

Overview: Background [4/20]

Overview: Topics of Interest: Foundations [5/20]

Overview: Topics of Interest: Language Mechanisms [6/20]

Overview: Topics of Interest: Logic and Security [7/20]

Overview: Topics of Interest: Cryptographic Protocols [8/20]

Overview: Topics of Interest: Current Techniques [9/20]

Overview: Course Project [10/20]

An example from last time: file:nichols_mark.pdf file:nichols_mark

An example from last time: file:pekkarinen_andrew.pdf

Overview: Course Project: Milestones [11/20]

Overview: Example Project: Cryptographic programming in Jif [12/20]

This is an example project from David Walker

Example Final Project Outline

Overview: Other Project Topics [13/20]

Example projects from David Walker

Overview: Your Job [14/20]

Intro [15/20]

Surveys

A Language-Based Approach to Security

by Fre Schneider, Greg Morrisett, and Rob Harper

Security Properties, Principles and Mechanisms

edited from slides by David Walker and Andrew Meyers

Tutorial on Language-Based Security

by Greg Morrisett

Attacking Malicious Code: A report to the Infosec Research Council

by Gary McGraw and Greg Morrisett

Security Automata: [16/20]

Some References

Enforceable Security Policies

Notes by Steve Rogers

Enforcing Non-safety Security Policies with Program Monitors

Composing Security Policies in Polymer

Temporal Aspects as Security Automata

Mark Nichol's project implementing security automata in AspectJ

And code

Security Automata: Polymer [17/20]

Polymer is available at http://www.cs.princeton.edu/sip/projects/polymer/

Uses aspect-oriented techniques to implement execution monitor.

Customer class-loader modifies java bytecodes while loading them to check specified policies.

Security Automata: Disallow Println [18/20]

public class TestPolicy extends Policy {
  public Suggestion query(Action a) {
    aswitch(a) {
      case <* *.*.println(..)>: return new HaltSuggestion(this, a);
      default: return new UnregSuggestion(this, a);
    }
  }

  public void accept(Suggestion s) {
    if(s.isHalt()) System.out.print("Halting target ; no printlns allowed!\n");
  }
}

Security Automata: Limit Open Files [19/20]

class LimitFiles extends Policy {
    private int openFiles = 0; 
    private int maxOpen = 0;
    LimitFiles(int max) {
       maxOpen = max;
    }
    Suggestion query(Action a) { 
      aswitch (a) {
        case <* *.*.fileOpen(..)>:
           if (++openFiles <= maxOpen) 
               return Suggestion.OK();
           else
               return Suggestion.Halt();
        case <* *.*.fileClose(..)>:
           --openFiles;
           return Suggestion.OK();
        default:
           return new UnregSuggestion(this, a);
      }
    }
}

Security Automata: [20/20]

class AndPolicy extends Policy {  
  private Policy p1;
  private Policy p2; 
  
  AndPolicy(Policy pol1, Policy pol2) {
    p1 = pol1;
    p2 = pol2;
  }
  Suggestion before(Action a) {

     Suggestion s1 = p1.before(a);
     Suggestion s2 = p2.before(a);
     if (s1.isOK() && s2.isOK())  
        return Suggestion.OK();  
     else ... 
  }
}

Revised: 2006/04/06 17:19