From Tarski to Hilbert

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento aproximado en Coq sobre geometría titulado From Tarski to Hilbert.

Sus autores son Gabriel Braun y Julien Narboux (de la Universidad de Estrasburgo, Francia).

Su resumen es

In this paper, we report on the formal proof that Hilbert’s axiom system can be derived from Tarski’s system. For this purpose we mechanized the proofs of the first twelve chapters of Schwabauser, Szmielew and Tarski’s book: Metamathematische Methoden in der Geometrie. The proofs are checked formally within classical logic using the Coq proof assistant. The goal of this development is to provide clear foundations for other formalizations of geometry and implementations of decision procedures.

El trabajo se ha presentado en el ADG 2012 (Automated Deduction in Geometry 2012)

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

Computer theorem proving and HoTT

PorJosé A. Alonso

Se ha publicado un artículo sobre la demostración asistida por ordenador y los fundamentos de la matemática titulado Computer theorem proving and HoTT.

Sus autores son Joe Leslie-Hurd (de Intel Corporation) y G. McC. Haworth (de la Universidad de Reading).

Su resumen es

Theorem-proving is a one-player game. The history of computer programs being the players goes back to 1956 and the ‘LT’ Logic Theory Machine of Newell, Shaw and Simon. In game-playing terms, the ‘initial position’ is the core set of axioms chosen for the particular logic and the ‘moves’ are the rules of inference. Now, the Univalent Foundations Program at IAS Princeton and the resulting ‘HoTT’ book on Homotopy Type Theory have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.

Formal verification of language-based concurrent noninterference

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Formal verification of language-based concurrent noninterference.

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (de la Universidad Técnica de Munich, Alemania).

Su resumen es

We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of non-interference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.

El trabajo se ha publicado en el Journal of Formalized Reasoning.

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

A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con PVS titulado A TCAS-II resolution advisory algorithm.

Sus autores son César Muñoz, Anthony Narkawicz y James Chamberlain (del
Langley Research Center de la NASA en Hampton, EE.UU.).

Su resumen es

The Traffic Alert and Collision Avoidance System (TCAS) is a family of airborne systems designed to reduce the risk of mid-air collisions between aircraft. TCAS II, the current generation of TCAS devices, provides resolution advisories that direct pilots to maintain or increase vertical separation when aircraft distance and time parameters are beyond designed system thresholds. This paper presents a mathematical model of the TCAS II Resolution Advisory (RA) logic that assumes accurate aircraft state information. Based on this model, an algorithm for RA detection is also presented. This algorithm is analogous to a conflict detection algorithm, but instead of predicting loss of separation, it predicts resolution advisories. It has been formally verified that for a kinematic model of aircraft trajectories, this algorithm completely and correctly characterizes all encounter geometries between two aircraft that lead to a resolution advisory within a given lookahead time interval. The RA detection algorithm proposed in this paper is a fundamental component of a NASA sense and avoid concept for the integration of Unmanned Aircraft Systems in civil airspace.

Este trabajo es parte del proyecto de la NASA Airborne Coordinated Resolution and Detection (ACCoRD) que está integrado en el proyecto Formal Analysis of Conflict Detection and Resolution Algorithms.

El trabajo se presentó el 19 de agosto en la AIAA Guidance, Navigation, and Control Conference.

Formal verification of cryptographic security proofs

PorJosé A. Alonso

Se ha publicado una tesis de verificación formal con Isabelle/HOL titulada Formal verification of cryptographic security proofs.

Su autor es Matthias Berg (de la Universidad de Sarre (en alemán: Saarland)) dirigido por Michael Backes.

Su resumen es

Verifying cryptographic security proofs manually is inherently tedious and error-prone. The game-playing technique for cryptographic proofs advocates a modular proof design where cryptographic programs called games are transformed stepwise such that each step can be analyzed individually. This code-based approach has rendered the formal verification of such proofs using mechanized tools feasible.

In the first part of this dissertation we present Verypto: a framework to formally verify game-based cryptographic security proofs in a machine-assisted manner. Verypto has been implemented in the Isabelle proof assistant and provides a formal language to specify the constructs occurring in typical cryptographic games, including probabilistic behavior, the usage of oracles, and polynomial-time programs. We have verified the correctness of several game transformations and demonstrate their applicability by verifying that the composition of 1-1 one-way functions is one-way and by verifying the IND-CPA security of the ElGamal encryption scheme.

In a related project Barthe et al. developed the EasyCrypt toolset, which employs techniques from automated program verification to validate game transformations. In the second part of this dissertation we use EasyCrypt to verify the security of the Merkle-Damgård construction – a general design principle underlying many hash functions. In particular we verify its collision resistance and prove that it is indifferentiable from a random oracle.