Verifikation der Speicherhandhabung in bestehenden C Programmen mit numerischen abstrakten Domänen.

• Applicant: Dr. Axel Simon
• Subject Area: Software Engineering and Programming Languages
• Term: from 2009 to 2014
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 154707536

• Final Report Year: 2016

Final Report Abstract

Die Programmanalyse, die in dem Projekt geschaffen werden sollte, basiert auf drei Säulen: der ersten Säule, die Maschinenkode einliest und Fixpunkte auf der abstrakten Semantik berechnet, der zweiten Säule, die den Arbeitsspeicher strukturiert und zusammenfasst und einer dritten Säule, die Variablen numerische Werte zuordnet. Das generelle Ziel des Projektes war es, eine verbesserte Prazision gegenuber Ansätzen in der Literatur zu erreichen, die es erlauben, die Abwesenheit von sicherheitskritischen Fehlern in existierender Software zu beweisen. Es konnten einige bekannte Sicherheitslücken in open-source Programmen nachgewiesen werden. Der erste eingesetzte Doktorand hat ein Werkzeug namens GDSL geschrieben, das Beschreibungen von Instruktionsdekodern und von semantischen Interpretationen von Instruktionen in effizienten C Kode übersetzt. Dieses Werkzeug hat der dritte Doktorand im Sommer 2016 in eine externe IT-Infrastruktur integriert, womit ein wichtiger Teil des Projektes industriell weiter genutzt wird. Der zweite Doktorand, der die Analyse von Datenstrukturen untersucht, hat einen Ansatz zur Zusammenfassung von einzelnen Variablen auf mehrere Variablen verallgemeinert, wie im Antrag auch vorgeschlagen wurde. Basierend auf diesen so genannten fold und expand Operatoren konnte eine Analyse von Datenstrukturen realisiert werden, die Listen, Bäume und Graphen unterscheiden kann, ohne dass der Benutzer entsprechende Invarianten vorgeben muss. Diese Analyse wurde erweitert, um auch die Inhalte von Heap Zellen einzubeziehen so dass, zum Beispiel, Invarianten von Suchbaumen von klassischen numerischen Domänen inferiert werden können. Beide Eigenschaften können mit den bisherigen Ansätzen von Separation Logic und Three-Valued Logic Analysis (TVLA) nur durch Vorgabe von recht spezifischen Invarianten bewiesen werden. Die in dem GDSL Werkzeug benutzte Domänen-spezifische Sprache hat auch den Rahmen für eine Erweiterung des Forschungsfeldes des Antragstellers geboten, nämlich auf die Anwendung von Techniken der Programmanalyse auf die Inferenz von Typen. Insbesondere konnte die expand Operation benutzt werden, um die Instantiierung von Typen in der Hindley-Milner Typinferenz zu erklären. Diese unerwartete Verbindung hat uns motiviert, die klassische Hindley-Milner Typinferenz mit der Inferenz von Vektor-Größen und dem Fluss von Feldern in sogenannten row polymorphic records zu erweitern. Diese Ideen wurden in dem GDSL Werkzeug implementiert, das damit eine sehr mächtige Typinferenz erhalten hat. Die Herleitung von Typsystemen durch Techniken der abstrakten Interpretation konnte mit der expand Operation eine semantische Basis gegeben werden, die die syntaktische Instantiierung von Typen per Substitutionen ablöst. Dadurch wird der Weg geebnet, Typinferenzen von der konkreten Semantik der Programmiersprache herzuleiten, was die Möglichkeit gibt, Optimalität der Inferenz zu hinterfragen und ultimativ zu erreichen. Um diesen Fragestellungen nachzugehen, wurde ein Microsoft SEIF grant eingeworben.

Publications

• Precise Static Analysis of Binaries by Extracting Relational Information. In M.Pinzger and D. Poshyvanyk, editors, Working Conference on Reverse Engineering, Limerick, Ireland, October 2011. IEEE
  A. Sepp, B. Mihaila, and A. Simon
  
• Inferring Definite Counterexamples Through Under-Approximation. In A. E. Goodloe and S. Person, editors, NASA Formal Methods, volume 7226 of LNCS, Norfolk, Virginia, USA, April 2012. Springer
  J. Brauer and A. Simon
  
• FESA: Fold- and Expand-based Shape Analysis. In Compiler Construction, volume 7791 of LNCS, pages 82–101, Rome, Italy, March 2013. Springer
  H. Siegel and A. Simon
  
• GDSL: A Universal Toolkit for Giving Semantics to Machine Language. In C. Shan, editor, Asian Symposium on Programming Languages and Systems, Melbourne, Australia, December 2013. Springer
  J. Kranz, A. Sepp, and A. Simon
  
• The Undefined Domain: Precise Relational Information for Entities that Do Not Exist. In C. Shan, editor, Asian Symposium on Programming Languages and Systems, Melbourne, Australia, December 2013. Springer
  H. Siegel, B. Mihaila, and A. Simon
  
• Widening as Abstract Domain. In NASA Formal Methods, volume 7871 of LNCS, pages 170–186, Moffett Field, California, USA, May 2013. Springer
  B. Mihaila, A. Sepp, and A. Simon
  
• Deriving a Complete Type Inference for Hindley-Milner and Vector Sizes using Expansion. Science of Computer Programming, 95, Part 2(0):254–271, 2014
  A. Simon
  
• Optimal Inference of Fields in Row-Polymorphic Records. In Programming Language Design and Implementation, SIGPLAN, Edinburg, UK, June 2014. ACM
  A. Simon
  
• Synthesizing Predicates from Abstract Domain Losses. In J. Badger and K. Y. Rosier, editors, NASA Formal Methods, volume 8430, pages 328–342, Houston, Texas, USA, April 2014. Springer
  B. Mihaila and A. Simon
  
• Shape Analysis with Connectors. In K. Havelund, G. J. Holzmann, and R. Joshi, editors, NASA Formal Methods, volume 9058 of LNCS, pages 343–358, Passadena, California, USA, April 2015. Springer
  H. Siegel and A. Simon