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.

Polygonal numbers in Mizar

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Mizar titulado Polygonal numbers in Mizar.

Su autor es Adam Grabowski (de la Universidad de Białystok, Polonia).

Su resumen es

In the article the formal characterization of triangular numbers (famous from [14] and words “EYPHKA! num = ∆ + ∆ + ∆”) [16] is given. Our primary aim was to formalize one of the items (42) from Wiedijk’s Top 100 Mathematical Theorems list, namely that the sequence of sums of reciprocals of triangular numbers converges to 2 and this Mizar representation was written in 2007. As the Mizar language evolved and attributes with arguments were implemented, we decided to extend these lines and we characterized polygonal numbers.

We formalized centered polygonal numbers, the connection between triangular and square numbers, and also some equalities involving Mersenne primes and perfect numbers. We gave also explicit formula to obtain from the polygonal number its ordinal index. Also selected congruences modulo 10 were enumerated. Our work basically covers the Wikipedia item for triangular numbers and
the Online Encyclopedia of Integer Sequences (http://oeis.org/A000217).

An interesting related result [15] could be the proof of Lagrange’s four-square theorem or Fermat’s polygonal number theorem [30].

El artículo se publicará en la revista Formalized Mathematics.