TU Darmstadt / ULB / TUprints

Sound Program Transformation Based on Symbolic Execution and Deduction

Ji, Ran :
Sound Program Transformation Based on Symbolic Execution and Deduction.
Technische Universität, Darmstadt
[Ph.D. Thesis], (2014)

[img]
Preview
Text
main.pdf
Available under Creative Commons Attribution Non-commercial No Derivatives, 2.5.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Title: Sound Program Transformation Based on Symbolic Execution and Deduction
Language: English
Abstract:

In this thesis, we are concerned with the safety and security of programs. The problems addressed here are the correctness of SiJa (a subset of Java) source code and Java bytecode, and the information flow security of SiJa programs. A lot of research has been made on these topics, but almost all of them study each topic independently and no approach can handle all of these aspects. We propose a uniform framework that integrates the effort of proving correctness and security into one process. The core concept for this uniform approach is sound program transformation based on symbolic execution and deduction. The correctness of SiJa source code is verified with KeY, a symbolic execution based approach. Partial evaluation actions are interleaved during symbolic execution to reduce the proof size. By synthesizing the symbolic execution tree achieved in the source code verification phase, we can generate a program that is bisimilar to, but also more optimized than, the original one with respect to a set of observable locations. The soundness of program transformation is proven. Apply the sound program transformation approach, we can generate a program bisimilar to the original program with respect to the low security level variables. This results in a more precise analysis of information flow security than the approaches based on security type systems. We can also generate Java bytecode from SiJa source code program transformation approach, where the the correctness of the Java bytecode is guaranteed and compiler verification is not necessary.

Alternative Abstract:
Alternative AbstractLanguage
Die vorliegende Arbeit beschäftigt sich mit der technischen Sicherheit (engl. Safety) sowie der Informationssicherheit (engl. Security) von Programmen. Im Speziellen betrachten wir die Korrektheit von SiJa-Programmen, einer Teilmenge von Java, im Quellcode und dem daraus erzeugten Java-Bytecode. In der aktuellen Forschung werden die einzelnen Aspekte fast ausschließlich getrennt behandelt. Das heißt, es wird nur die technische Sicherheit oder nur die Informationssicherheit von Programmen betrachtet und dann entweder nur mit Bezug auf den Quellcode oder nur für das kompilierte Programm. Wir schlagen stattdessen ein Rahmenwerk vor, das die unterschiedlichen Aspekte in einem einzigen Prozess vereint. Die Grundidee des Rahmenwerks ist ein einheitlicher Ansatz zur beweisbar korrekten Programmtransformation unter Anwendung von Techniken aus der Deduktion sowie der symbolischen Programmausführung. Mithilfe von KeY werden die SiJa-Programme (im Quellcode) verifiziert und deren Korrektheit sichergestellt. Die Verifikationstechnik beruht auf symbolischer Ausführung. Um die Korrektheitsbeweise klein zu halten, werden abwechselnd Programmspezialisierungsschritte und symbolische Ausführungsschritte angewendet. Aus dem während der Verifikationsphase konstruierten symbolischen Ausführungsbaum erzeugen wir ein zum Ursprungsprogramm bezüglich des beobachtbaren Programmzustandes äquivalentes und optimiertes transformiertes Programm. Die Korrektheit der Programmtransformation wird in dieser Arbeit bewiesen. Ferner wenden wir diesen Ansatz an, um ein Programm zu generieren, welches bezüglich Variablen mit einer niedrigen Sicherheitsstufe das gleiche Verhalten aufweist wie das ursprüngliche Programm. Damit ist es uns möglich eine präzisiere Informationsflussanalyse zu realisieren als vergleichbare typ-basierte Systeme. Des weiteren erlaubt das Rahmenwerk SiJa-Quellcode in Java-Bytecode zu kompilieren, ohne das dessen Korrektheit bewiesen werden muss, da sie aus der Verifikation des Quellcodes folgt. Insbesondere ist dank unseres Ansatzes eine Verifikation des Compilers nicht notwendig.German
Place of Publication: Darmstadt
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: 20 Department of Computer Science
Date Deposited: 24 Jun 2014 14:11
Last Modified: 24 Jun 2014 14:11
URN: urn:nbn:de:tuda-tuprints-40211
Referees: Hähnle, Prof. Dr. Reiner and Beckert, Prof. Dr. Bernhard
Refereed: 18 December 2013
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/4021
Export:
Actions (login required)
View Item View Item

Downloads

Downloads per month over past year