[Cryptography] Security proofs prove non-failproof

[Jonathan Thornburg]

On Mon, Feb 20, 2017 at 03:29:34PM -0800, Bill Frantz wrote:
[[about when formal methods will be more widely used]]
> The critical mass is probably when someone reports that they saved real
> money using formal methods to achieve a level of software reliability.

I think we're already there: Airbus uses formal methods to verify
parts of the fly-by-wire flight-control software for its airliners:

"Formal Verification of Avionics Software Products"
Jean Souyris, Virginie Wiels, David Delmas, and Herve Delseny
Abstract:
  This paper relates an industrial experience in the field of formal
  verification of avionics software products. Ten years ago we
  presented our very first technological research results in [18].
  What was just an idea plus some experimental results at that time
  is now an industrial reality. Indeed, since 2001, Airbus has been
  integrating several tool supported formal verification techniques
  into the development process of avionics software products. Just
  like all aspects of such processes, the use of formal verification
  techniques must comply with DO-178B [9] objectives and Airbus has
  been a pioneer in this domain.
Keywords:
  avionics software, safety, development process, verification,
  formal verification, Abstract Interpretation, static analysis
published in
  A. Cavalcanti and D. Dams (Eds.): FM 2009, Springer Lecture Notes
  in Computer Science volume 5850, pp. 532--546 (2009)
  http://www.springerlink.com/content/0265621453714708/fulltext.pdf

Another interesting paper from Airbus is:

"Towards Formally Verified Optimizing Compilation in Flight Control Software"
Ricardo Bedin Franca, Denis Favre-Felix, Xavier Leroy, Marc Pantel,
and Jean Souyris
Abstract:
  This work presents a preliminary evaluation of the use of the
  CompCert formally specified and verified optimizing compiler for
  the development of level A critical flight control software. First,
  the motivation for choosing CompCert is presented, as well as the
  requirements and constraints for safety-critical avionics software.
  The main point is to allow optimized code generation by relying on
  the formal proof of correctness instead of the current un-optimized
  generation required to produce assembly code structurally similar
  to the algorithmic language (and even the initial models) source
  code. The evaluation of its performance (measured using WCET) is
  presented and the results are compared to those obtained with the
  currently used compiler. Finally, the paper discusses verification
  and certification issues that are raised when one seeks to use
  CompCert for the development of such critical software.
published in
  "Predictability and Performance in Embedded Systems : PPES 2011"
  volume 18 (2011) 59--68
  http://dx.doi.org/10.4230/OASIcs.PPES.2011.59
  http://hal.inria.fr/docs/00/55/13/70/PDF/pppes2011_2112.pdf

ciao,
-- 
-- "Jonathan Thornburg [remove -animal to reply]" <jthorn at astro.indiana-zebra.edu>
   Dept of Astronomy & IUCSS, Indiana University, Bloomington, Indiana, USA
   "There was of course no way of knowing whether you were being watched
    at any given moment.  How often, or on what system, the Thought Police
    plugged in on any individual wire was guesswork.  It was even conceivable
    that they watched everybody all the time."  -- George Orwell, "1984"