POLICY MEETING
July 21, 1999
3085 ENG II
3:00-4:00pm
In attendance:
Karl Levitt (KL), Michael Gertz (MG), Nicole Carlson (NC), Jim Hoagland (JH), Aaron Keen (AK), Dave Peticolas (DP), Mark Heckman (MH), and Brant Hashii (BH)
- Release of DARPA BAA 99-33
- Coalition partners - temporarily our allies
- Submit a proposal with Rich Fiertag and on our own
- Policy Projection - compile abstract policy down into enforcement policies
- Use a standard language
- Jim's language LaSCO would be a good starting point. It's readable and you can write detailed policies from it
- Apply CISL
- UML - derivation of state charts, composition rules; composing state machines
- DAPA likes broad-applicability - prototypes, many applicable systems
- McLean's paper: "A General Theory of Composition for Trace Sets Closed Under Selective Interleaving Functions"
- Uses Alpern-Schneider framework
- Model set of states, properties of systems
- Safety properties - predicate on a state
- Liveness properties - eventually true in state
- Show implementation satisfies specification
- Non-interference Property (Abadi/Lamport) - low level and high-level security
- Separability
- Theory about Security Policy - interleaving function
- 3 external composing constructs
- Product - running two systems in parallel that don't interact (run independently)
- Cascade - running two systems in serial. Theorems about how security policies are preserved under cascade.
- Feedback - circular construction. Hits both systems twice before exiting to an external
- Theorems of composing systems
- Not as clean as cascade
- Separability and non-interference
- 3 Internal Composition Constructs - Restrictiveness (Abadi/Lamport)
- Trace Union, Intersection, Difference
- Need restrictiveness assumption to preserve high level security properties
- For Next Week
- Jim will present a review of his LaSCO work
- Brainstorm Policy topic for BAA