Download Sound Program Transformation Based on Symbolic Execution and Deduction PDF

TitleSound Program Transformation Based on Symbolic Execution and Deduction
LanguageEnglish
File Size1.0 MB
Total Pages118
Table of Contents
                            Abstract
Acknowledgment
Introduction
	Overview: Software Correctness and Security
	Problems and Contributions
	Publications
Background
	KeY and Symbolic Execution
	Programming Language
	Program Logic
	Sequent Calculus
Partial Evaluation
	Partial Evaluation
	Interleaving Symbolic Execution and Partial Evaluation
		General Idea
		The Program Specialization Operator
		Specific Specialization Actions
	Example
	Evaluation
Program Transformation
	Weak Bisimulation Relation of Programs
	The Weak Bisimulation Modality and Sequent Calculus Rules
	Soundness
	Optimization
		Sequentialized Normal Form of Updates
		Sequent Calculus Rules Involving Updates
	Implementation and Evaluation
Information Flow Security
	Introduction
	Enforcing Information Flow Security by Program Transformation
Deductive Compilation
	Introduction
	Sequent Calculus for Bytecode Generation
	Example
Conclusion
	Summary
	Future Work
Bibliography
                        
Document Text Contents
Page 59

must be reflected in the observable locations of the loop body. The result of this phase is a
symbolic execution tree as illustrated in Figure 2.11.

Phase 2. We synthesize the target program q and used variable set use from qi and usei
by applying the rules in a leave-to-root manner. One starts with a leaf node and generates
the program within its sequential block first, e.g., bl

3

, bl
4

, bl
5

, bl
6

in Figure 2.11. These
are combined by rules corresponding to statements that contain a sequential block, such as
loopInvariant (containing bl

3

and bl
4

). One continues with the generalized sequential block
containing the compound statements, e.g., GSB(bl

2

), and so on, until the root is reached. Note
that the order of processing the sequential blocks matters, for instance, the program for the
sequential block bl

4

must be generated before that for bl
3

, because the observable locations in
node n

3

depend on the used variable set of bl
4

according to the loopInvariant rule.

We explain some of the rules in details.

emptyBox

�=)[email protected](obs, _)�,�
�=)U [ _ « _ ]@(obs, obs)�,�

The emptyBox rule is the starting point of program transformation in each sequential block.
The location set use is set to obs, which is the direct result of Lemma 4.

assignment

�=)U {l := r}[! « ! ]@(obs, use)�,�

�=)U [ l= r;! « l= r;! ]@(obs, use� {l}[ {r})�,� if l 2 use
�=)U [ l= r;! « ! ]@(obs, use)�,� otherwise

!

In the assignment rule, the use set contains all program variables on which a read access might
occur in the remaining program before being overwritten. In the first case, when the left side
l of the assignment is among those variables, we have to update the use set by removing the
newly assigned program variable l and adding the variable r which is read by the assignment.
The second case makes use of the knowledge that the value of l is not accessed in the remaining
program and skips the generation of the assignment.

ifElse

�,U b=)U [ p;! « p;! ]@(obs, use
p;!)�,�

�,U¬b=)U [ q;! « q;! ]@(obs, use
q;!)�,�

�=)U [ if (b) {p} else {q} ! «
if (b) {p;!} else {q;!} ]@(obs, use

p;! [ useq;! [ {b})�,�
(with b boolean variable)

49

Page 60

On encountering a conditional statement, symbolic execution splits into two branches, namely
the then branch and else branch. The generation of the conditional statement will result in
a conditional. The guard is the same as used in the original program, the then branch is the
generated version of the source then branch continued with the rest of the program after the
conditional, and the else branch is analogous to the then branch.

Note that the statements following the conditional statement are symbolically executed on
both branches. This leads to duplicated code in the generated program, and, potentially to
code size duplication at each occurrence of a conditional statement. One note in advance: code
duplication can be avoided when applying a similar technique as presented later in connection
with the loop translation rule. However, it is noteworthy that the application of this rule might
have also advantages: as discussed in Chapter 3, symbolic execution and partial evaluation can
be interleaved resulting in (considerably) smaller execution traces. Interleaving symbolic execu-
tion and partial evaluation is orthogonal to the approach presented here and can be combined
easily. In several cases this can lead to different and drastically specialized and therefore smaller
versions of the remainder program ! and !. The use set is extended canonically by joining the
use sets of the different branches and the guard variable.

loopInvariant

�=)U inv,�
�,UVmod(b^ inv) =)UVmod

[ p « p ]@(use
1

[ {b}, use
2

)inv,�
�,UVmod(¬b^ inv) =)UVmod[! « ! ]@(obs, use1)�,�

�=)U [ while(b){p}! « while(b){p}! ]@(obs, use
1

[ use
2

[ {b})�,�

On the logical side the loop invariant rule is as expected and has three premises. Here we are
interested in compilation of the analyzed program rather than proving its correctness. There-
fore, it is sufficient to use true as a trivial invariant or to use any automatically obtainable
invariant. In this case the first premise (init) ensuring that the loop invariant is initially valid
contributes nothing to the program compilation process and is ignored from here onward (if
true is used as invariant then it holds trivially).

Two things are of importance: the third premise (use case) executes only the program fol-
lowing the loop. Furthermore, this code fragment is not executed by any of the other branches
and, hence, we avoid unnecessary code duplication. The second observation is that variables
read by the program in the third premise may be assigned in the loop body, but not read in the
loop body. Obviously, we have to prevent that the assignment rule discards those assignments
when compiling the loop body. Therefore, in the obs for the second premise (preserves), we
must include the used variables of the use case premise and, for similar reasons, the program
variable(s) read by the loop guard. In practice this is achieved by first executing the use case

50

Page 117

[Mey86] Bertrand Meyer. Design by contract. Technical Report TR-EI-12/CO, pages 1–50,
1986.

[Mey92] Bertrand Meyer. Applying “design by contract”. IEEE Computer, 25(10):40–51,
October 1992.

[Mey00] Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, 2000.

[Mos05] Wojciech Mostowski. Formalisation and verification of Java Card security properties
in dynamic logic. In Maura Cerioli, editor, Proc. Fundamental Approaches to Software
Engineering (FASE), Edinburgh, volume 3442 of LNCS, pages 357–371. Springer,
April 2005.

[MP67] John Mccarthy and James Painter. Correctness of a compiler for arithmetic expres-
sions. In Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia
in Applied Mathematics, pages 33–41. American Mathematical Society, 1967.

[MPH00] Jörg Meyer and Arnd Poetzsch-Heffter. An architecture for interactive program
provers. In TACAS, pages 63–77, 2000.

[MW72] Robin Milner and Richard Weyhrauch. Proving compiler correctness in a mecha-
nized logic. In Proc. 7th Annual Machine Intelligence Workshop, volume 7 of Machine
Intelligence, pages 51–72. Edinburgh University Press, 1972.

[Mye04] Glenford J. Myers. Art of Software Testing. John Wiley & Sons, second edition, 2004.

[NPW02] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof
Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

[Plo04] Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr.
Program., 60-61:17–139, 2004.

[Pra76] Vaughan R. Pratt. Semantical considerations on floyd-hoare logic. In FOCS, pages
109–121, 1976.

[PV04] Corina S. Pasareanu and Willem Visser. Verification of Java programs using symbolic
execution and invariant generation. In Susanne Graf and Laurent Mounier, editors,
Proc. Model Checking Software, 11th International SPIN Workshop, Barcelona, Spain,
volume 2989 of LNCS, pages 164–181. Springer, 2004.

[Rey02] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In
LICS, pages 55–74, 2002.

[Rüm06] Philipp Rümmer. Sequential, parallel, and quantified updates of first-order struc-
tures. In Miki Hermann and Andrei Voronkov, editors, Proc. Logic for Programming,

107

Similer Documents