Princeton’s ABPL model

• Formal description of Java’s access control system

• Concepts

  • principal (P)
    • with conjunctions
  • target (T)
  • statement (P says s)
  • quotation
  • authority

• Map Java stack inspection into ABPL

• Termination Theorem

  • always terminates

• Soundness Theorem

  • ABPL proofs for trues

• Completeness Conjecture

• Equivalence Theorem

Previous slide

Next slide

Back to first slide

View graphic version