I am looking for a formal characterization of Capability-based security in Isabelle/HOL using a set of invariants that "is complete". I'm not exactly sure what "complete" means, and I'm also not sure if my starting point makes sense:

theory Capability_Security
imports Main

type_synonym user_id = nat
type_synonym object_id = nat
type_synonym capability = "user_id × object_id ⇒ bool"

definition is_valid_cap :: "user_id ⇒ object_id ⇒ capability ⇒ bool" where
"is_valid_cap uid oid cap ≡ cap (uid, oid)"

definition can_access :: "user_id ⇒ object_id ⇒ capability ⇒ bool" where
"can_access uid oid cap ≡ ∃owner. is_valid_cap owner oid cap ∧
  (owner = uid ∨ cap (uid, owner))"

definition secure_system :: "capability set ⇒ bool" where
"secure_system caps ≡ ∀uid oid1 oid2 cap1 cap2. is_valid_cap uid oid1 cap1 ∧
  is_valid_cap uid oid2 cap2 ∧ oid1 ≠ oid2 ∧ ¬can_access uid oid2 cap1 ∧
  ¬can_access uid oid1 cap2 ⟶ ¬(cap1 = cap2)"

I'm not sure if above is enough, but I'd be glad for any hints or pointers that might allow me to make progress. Thanks!

One thing I'm specifically after (well, if the definitions make sense) are invariants that are commonly agreed to be necessary and sufficient, such as

theorem access_monotonicity:
  assumes "secure_system caps"
  assumes "can_access uid oid cap"
  assumes "cap ⊆ cap'"
  shows "can_access uid oid cap'"

This invariant states that if a user can access an object with a given capability, they can also access the object with a superset of that capability. This invariant is important because it ensures that if a user has access to an object, they can also access the object with a more permissive capability.

  • 1
    $\begingroup$ It might help to ask a more general question: what are some formalizations of security in Isabelle/HOL? I am sure there are some, but I don't know any specifically. There ought to be people around here who do. $\endgroup$ Feb 17, 2023 at 17:10
  • $\begingroup$ yeah, any formalization in Isabelle/HOL of any security model (eg RBAC or other) would probably help! and any formalization (in sth different than Isabelle/HOL) of capability-based security as well. if only a commonly used/agreed list of invariants that capability-based security must fulfil. $\endgroup$
    – oberstet
    Feb 17, 2023 at 22:21
  • 2
    $\begingroup$ I'd start digging for security-related content in the Archive of Formal Proofs. $\endgroup$
    – Kai
    Feb 23, 2023 at 6:57
  • $\begingroup$ seL4's access control system is based on capabilities, here is a high-level overview which may be of interesting. $\endgroup$
    – Wno-all
    Mar 14, 2023 at 22:21


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.