Reseña: Principles for verification tools: Separation logic

PorJosé A. Alonso

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í.

Reseña: The Unified Policy Framework (UPF)

PorJosé A. Alonso

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

Sus autores son

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í.

Reseña: Real-valued special functions: upper and lower bounds

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Real-valued special functions: upper and lower bounds

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

This development proves upper and lower bounds for several familiar real-valued functions. For sin, cos, exp and sqrt, it defines and verifies infinite families of upper and lower bounds, mostly based on Taylor series expansions. For arctan, ln and exp, it verifies a finite collection of upper and lower bounds, originally obtained from the functions’ continued fraction expansions using the computer algebra system Maple. A common theme in these proofs is to take the difference between a function and its approximation, which should be zero at one point, and then consider the sign of the derivative. The immediate purpose of this development is to verify axioms used by MetiTarski, an automatic theorem prover for real-valued special functions. Crucial to MetiTarski’s operation is the provision of upper and lower bounds for each function of interest.

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

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

Reseña: Combining proofs and programs in a dependently typed language

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado [Combining proofs and programs in a dependently typed language](

Sus autores son Chris Casinghino, Vilhelm Sjöberg y Stephanie Weirich (de la Universidad de Pensilvania, EE.UU.).

Su resumen es

Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Ωmega. Here, we combine these two approaches into a single dependently-typed core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and “mobile” program values, including proofs computed at runtime, may be used as evidence by the logic. This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.

El trabajo se presentó en el POPL 2014 (41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages).

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

Reseña: Mechanized network origin and path authenticity proofs

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Mechanized network origin and path authenticity proofs.

Sus autores son Fuyuan Zhang, Limin Jia, Cristina Basescu, Tiffany Hyun-Jin Kim, Yih-Chun Hu y Adrian Perrig.

Su resumen es

A secure routing infrastructure is vital for secure and reliable Internet services. Source authentication and path validation are two fundamental primitives for building a more secure and reliable Internet. Although several protocols have been proposed to implement these primitives, they have not been formally analyzed for their security guarantees. In this paper, we apply proof techniques for verifying cryptographic protocols (e.g., key exchange protocols) to analyzing network protocols. We encode LS 2, a program logic for reasoning about programs that execute in an adversarial environment, in Coq. We also encode protocol-specific data structures, predicates, and axioms. To analyze a source-routing protocol that uses chained MACs to provide origin and path validation, we construct Coq proofs to show that the protocol satisfies its desired properties. To the best of our knowledge, we are the first to formalize origin and path authenticity properties, and mechanize proofs that chained MACs can provide the desired authenticity properties.

El trabajo se presentará en el ACM CCS 2014 (21st ACM Conference on Computer and Communications Security).

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