Research proof index

The verifyAlwaysAllows analysis is sound: if the assertions verifyAlwaysAllows ps₁ εnv are unsatisfiable for the policies ps₁ and the strongly well-formed symbolic environment εnv, then the authorizer will return allow when applied to ps₁ and any strongly well-formed concrete environment env ∈ᵢ εnv.

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then verifyAlwaysAllows and verifyAlwaysAllowsOpt are equivalent.

The verifyAlwaysDenies analysis is sound: if the assertions verifyAlwaysDenies ps₁ εnv are satisfiable for the policies ps₁ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the authorizer will not return deny when applied to ps₁ and env.

Concrete version of verifyAlwaysDenies_is_complete.

Concrete version of verifyAlwaysDenies_is_sound.

The verifyAlwaysDenies analysis is sound: if the assertions verifyAlwaysDenies ps₁ εnv are unsatisfiable for the policies ps₁ and the strongly well-formed symbolic environment εnv, then the authorizer will return deny when applied to ps₁ and any strongly well-formed concrete environment env ∈ᵢ εnv.