SE547: Lecture 1 (Security Automata)

• Security Properties / Security Automata
• Access Control
• Information Flow
• Crytographic Protocols
• More TBD

Foundations of Computer Security is for

• students interested in programming languages and how to apply them to solving systems security problems
• students interested in systems security problems and how to use programming languages to solve them

• Some lectures given by me on technical topics
• Some discussions of papers on security
  • class participation is important
• Occasional homework, such as a 1-page writing assignment summarizing or critiquing a paper

• It will be useful to have some background in logic or language semantics
• I will try to fill in background as I go

• what is security?
  • safety, liveness, secrecy, authenticity, integrity
• what principles are available that help us build secure systems?
  • open design, economy of mechanism, minimal trusted computing base, etc

• dynamic program monitoring
  • theory: what kind of properties can we enforce?
  • practice: languages for writing program monitors
• static program analysis
  • type systems for safe virtual machines
  • enforcing information flow properties

• specifying security properties logically
  • authentication logics
  • proof-carrying authorization
  • security for distributed logic programs

• Specification of cryptographic protocols
  • make assumptions about the power of cryptographic primitives
  • nothing about cryptography itself
  • reasoning about cryptographic protocols using types

• Java security
  • class loaders, security managers, security policies for Java
  • stack inspection: what is it? How does it work? What kind of security does it really provide?
• Program analysis and security
  • model checkers: how to analyze one million lines of code for security flaws!
  • language designs: CQual, Vault

• A substantial project involving programming languages and security in some fashion
  • work alone or in pairs (alone if doing a survey)
  • once you get started: work steadily every week of the term (5-10 hours/week, perhaps more)
  • 1-1.5 hour presentations, starting in week 7 or 8.

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

An example from last time: file:pekkarinen_andrew.pdf

• week 4: Project prospectus (approx 1 page)
• week 6: Progress report due (approx 4 pages)
• week 7-10: present work
  • assign 1 or 2 papers to the class to read; give a lecture and discuss
• week 11: Final paper due
  • submit final report which includes introduction, problem description, technical accomplishments, any code, performance evaluation, related work, and summary

This is an example project from David Walker

• Jif is a programming language based on Java equipped with a type system for detecting information-flow.
• Learn about how Jif works, its features and semantics
• Use Jif:
  • Design an interface to a cryptographic library using Jif's decentralized label model.
  • Use the resulting library to implement the cryptographic protocols used in a secure client-server setting.
• Evaluate: What did you learn? Jif pros and cons?
• Starting points on the projects page:
  • eg: Jif Homepage http://www.cs.cornell.edu/jif/

Example Final Project Outline

• Abstract
• Section I: Introduction
  • Motivation (argument that makes the contributions seem inevitable!)
    • Information security is important.
    • Cryptographic primitives are crucial for network-based security.
    • Language-based security is practical way to increase confidence in security
    • Current support for cryptographic primitives in languages is not good.
  • Contributions
    • Design of a cryptographic library in Jif
    • Show how type system can encode desirable invariants
    • Investigation of event driven vs. threaded programs with information flow
    • Implementation of a (reasonably) substantial system using Jif
• Section II: Background material
  • Jif and Decentralized Label Model
    • Important features (label abstraction, first-class principals, declassification, endorsement), syntax, semantics
  • Cryptographic operations
• Section III: Design of the Cryptographic Library
  • Problems: Keeping keys secret; Dependency between keys and encrypted values; Authentication information encoded in the types; Integrity Constraints in Jif
  • Solutions: Dynamic Principals; Label polymorphism; Fancy programming
• Section IV: Evaluation of the Library
  • Description of the test case
    • Bank/ATM simulation with interesting authentication protocols
  • Implementation details/examples
  • Insights learned? Design choices you would have changed?
• Section V: Related Work
• Section VI: Conclusion
  • Summarize introduction
  • Reiterate contributions

Example projects from David Walker

• secure distributed programming and PlanetLab
  • implement a service for PlanetLab using an interesting programming model
    • tuple spaces (see Klaim for Java)
    • join calculus (see JoCaml)
    • distributed logic programming (see SD3, Sophia)
  • consider the security threats and the mechanisms necessary to compensate
  • implement a security monitoring service (as opposed to an arbitrary service)
• security monitors
  • a security monitor watches a program, virtual machine or distributed system and interrupts the system when it detects a security violation
  • consider security monitors based on transactions
    • theory of what is enforceable in the transactional model
    • practice of implementing the system
  • consider concurrent or distributed security monitors
  • consider hardware/compiler support for parallelizing execution of security monitors with the mainline application
  • consider type-system support for making security monitors compose with one another; implement it in the context of Polymer
• Verifying availability properties
  • recently, researchers have a great progress verifying cryptographic protocols and establishing authenticity and secrecy properties
    • Multi-set writing protocols (Cervesato et al.)
    • Types for protocols (Gordon and Jeffrey)
  • can we do the same for availability properties and developing robust distributed algorithms?
    • eg: can we developed techniques for verifying consensus and other group communication protocols? Under what failure models?
• Study the effectiveness of security analysis tools
  • How do we evaluate security analysis tools to determine how effective they are?
  • What properties should they have?
  • What metrics can we use to analyze tools?
  • Can we develop a benchmark for testing these tools?
  • Take two or more existing tools and analyze them.
• Extend a programming language
  • Polymer is a compiler framework for extending Java
    • add some form of program monitors based on automata
    • add Cryptic-like support to Java for verifying cryptographic protocols
  • Binder is a logic-programming language with built-in secuiry
    • implement a linear-logic programming version of binder
• information flow
  • consider tracking information flow in a unique programming model
    • tuple space model
    • distributed logic programming model
    • typed assembly language
• Survey paper option
  • choose a relatively broad area and do an in-depth analysis of the research in the area
    • come up with a creative way to classify the work in the area
    • summarize the major contributions
    • determine the most important avenues for future research
  • focus on producing a particularly well-written report by working on multiple drafts
  • eg: software program monitors; hardware support for security; security in distributed programming models
• Come up with a own topic related to your own research
  • Good topics may bridge gaps between areas
    • Networking and distributed programming
    • Algorithms for reliable computing and cryptography and languages to support their implementation or verification
    • Architecture or compilers to improve performance of security mechanisms

• In the next few days, figure out who you want to work with and what general topic you want to work on
• work with someone who has the same level of commitment to the course
• visit the course web page for ideas; talk with your friends or other people in the department; skim a couple of papers
• Discuss with me by phone Monday April 10 or Tuesday April 11.

  773-458-6577 Leave message if no answer, or make an appointment by email

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

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

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.

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

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

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