Fwd: Formal verification of high-level language implementation of critical software?
Forwarding on behalf of David von Oheimb <David.von.Oheimb@siemens.com>.
------------------------------------------------------------------------
Subject: Formal verification of high-level language implementation of critical software? From: David von Oheimb <David.von.Oheimb@siemens.com> Date: Mon, 09 Feb 2009 11:49:08 +0100 To: members@fmeurope.org, formal-methods@cs.uidaho.edu, fmacademic@cas.mcmaster.ca, haskell@haskell.org CC: Jorge Cuéllar <Jorge.Cuellar@siemens.com>, Greg Kimberly <Greg.Kimberly@boeing.com>
Dear all,
at Siemens Corporate Technology we are currently doing a study with Boeing on how to enhance assurance of open-source security-critical software components like OpenSSL. Methods considered range from standard static analysis tools to formal verification.
One observation is that the higher the programming language used is, the less likely programming mistakes are, and the easier a formal model can be obtained and the more likely it is to be faithful and verifiable. In this sense, implementations e.g. in a functional/logic programming language would be ideal.
Are you aware of any (security critical or other) software component that has been implemented in such a high-level language and has been formally verified? Any quick pointers etc. are appreciated.
Thanks, David v.Oheimb
+------------------------------------------------------------------<><-+ | Dr. David von Oheimb Senior Research Scientist | | Siemens AG, CT IC 3 Phone : +49 89 636 41173 | | Otto-Hahn-Ring 6 Fax : +49 89 636 48000 | | 81730 München Mobile: +49 171 8677 885 | | Germany E-Mail: David.von.Oheimb@siemens.com | | http://scd.siemens.de/db4/lookUp?tcgid=Z000ECRO http://ddvo.net/ |
Hi, Maybe not that "big" components, but we verified formally (in Isabelle/HOL) some decision procedure implementations (mainly quantifier elimination for linear real, integer arithmetic and their combination). Using Isabelle's push button Technology you transform the formally Isabelle/HOL implementation in to SML, Ocaml or Haskell. Here are some pointers: http://www.cl.cam.ac.uk/~ac638/pubs/pdf/mir.pdf http://www.cl.cam.ac.uk/~ac638/pubs/pdf/frpar.pdf http://www.cl.cam.ac.uk/~ac638/pubs/pdf/linear.pdf Best wishes, Amine. Simon Marlow wrote:
Forwarding on behalf of David von Oheimb <David.von.Oheimb@siemens.com>.
------------------------------------------------------------------------
Subject: Formal verification of high-level language implementation of critical software? From: David von Oheimb <David.von.Oheimb@siemens.com> Date: Mon, 09 Feb 2009 11:49:08 +0100 To: members@fmeurope.org, formal-methods@cs.uidaho.edu, fmacademic@cas.mcmaster.ca, haskell@haskell.org CC: Jorge Cuéllar <Jorge.Cuellar@siemens.com>, Greg Kimberly <Greg.Kimberly@boeing.com>
Dear all,
at Siemens Corporate Technology we are currently doing a study with Boeing on how to enhance assurance of open-source security-critical software components like OpenSSL. Methods considered range from standard static analysis tools to formal verification.
One observation is that the higher the programming language used is, the less likely programming mistakes are, and the easier a formal model can be obtained and the more likely it is to be faithful and verifiable. In this sense, implementations e.g. in a functional/logic programming language would be ideal.
Are you aware of any (security critical or other) software component that has been implemented in such a high-level language and has been formally verified? Any quick pointers etc. are appreciated.
Thanks, David v.Oheimb
+------------------------------------------------------------------<><-+ | Dr. David von Oheimb Senior Research Scientist | | Siemens AG, CT IC 3 Phone : +49 89 636 41173 | | Otto-Hahn-Ring 6 Fax : +49 89 636 48000 | | 81730 München Mobile: +49 171 8677 885 | | Germany E-Mail: David.von.Oheimb@siemens.com | | http://scd.siemens.de/db4/lookUp?tcgid=Z000ECRO http://ddvo.net/ |
Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
participants (2)
-
Amine Chaieb -
Simon Marlow