Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Principles for verification tools: Separation logic

Sus autores son Brijesh Dongol, Victor B. F. Gomes y Georg Struth (de la Universidad de Sheffield).

Su resumen es

A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data flow is captured by concrete store/heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof as- sistant simple and highly automatic. The resulting tool is correct by construction; it is explained on the classical linked list reversal example.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre seguridad titulado The Unified Policy Framework (UPF)

Sus autores son

• Achim D. Brucker (de SAP SE).
• Lukas Brügger (del ETH Zürich) y
• Burkhart Wolff (de la University Paris-Sud (Orsay))

Su resumen es

We present the Unified Policy Framework (UPF), a generic framework for modelling security (access-control) policies. UPF emphasizes the view that a policy is a policy decision function that grants or denies access to resources, permissions, etc. In other words, instead of modelling the relations of permitted or prohibited requests directly, we model the concrete function that implements the policy decision point in a system. In more detail, UPF is based on the following four principles: 1) Functional representation of policies, 2) No conflicts are possible, 3) Three-valued decision type (allow, deny, undefined), 4) Output type not containing the decision only.

El marco en el que se apoya el trabajo se presenta en la tesis de Lukas Brügger A framework for modelling and testing of security policies.

El trabajo se ha publicado en The Archive of Formal Proofs.

El código de las correspondientes teorías en Isabelle se encuentra aquí.