A term rewrite system framework for code carrying theory

UNIVERSIT´ A DEGLI STUDI DI PISA Dipartimento di Informatica Laurea Specialistica In Informatica & UNIVERSIDAD POLIT´ ECNICA DE VALENCIA Depto. Sistemas Inform´aticos y Computaci´on Ingenier´ıa Inform´atica THESIS A Term Rewrite System Framework for Code Carrying Theory CANDIDATE: SUPERVISORS: Paolo Picci Mar´ıa Alpuente Frasnedo Giorgio Levi July, 2011 Dipartimento di Informatica Universit´a di Pisa Via F. Buonarroti, 2 I-56127 Pisa, Itala Departamento de Sistemas Inform´aticos y Computaci´on Universidad Polit´ecnica de Valencia Camino de Vera, s/n 46022 Valencia, Spain Contents 1 Introduction 1 1.1 PlanoftheThesis. ........................ 2 2 Background on Term Rewriting 5 2.1 Terminology and definitions . . . . . . . . . . . . . . . . . . . 5 2.2 TermRewriting.......................... 6 3 The Rewrite Framework 9 3.1 Introduction............................ 9 3.2 Narrowing in Rewriting Logic . . . . . . . . . . . . . . . . . . 10 3.3 Transforming Rewrite Theories . . . . . . . . . . . . . . . . . 12 3.3.1 Definition Introduction . . . . . . . . . . . . . . . . . . 12 3.3.2 Definition Elimination . . . . . . . . . . . . . . . . . . 14 3.3.3 Folding........................... 14 3.3.4 Unfolding ......................... 16 3.3.5 Abstraction ........................ 17 3.4 Program Semantics and Correctness of the transformation system................................. 18 4 Rewrite on Code Carrying Theory 21 4.1 BackgroundonCCT ....................... 21 4.1.1 Code-Carrying Theory Steps . . . . . . . . . . . . . . . 23 4.2 Program Synthesis and CCT . . . . . . . . . . . . . . . . . . . 25 4.2.1 Certificate......................... 25 4.2.2 Steps on new framework . . . . . . . . . . . . . . . . . 26 i 4.2.3 Case Study: a tail recursive function . . . . . . . . . . 28 5 Security attacks and extension of the framework 31 5.1 Security .............................. 31 5.1.1 Hacking the certificate . . . . . . . . . . . . . . . . . . 34 5.2 Checking the Certificate . . . . . . . . . . . . . . . . . . . . . 37 5.2.1 Preconditions ....................... 38 6 Pyconnect 43 6.1 Description and Motivation . . . . . . . . . . . . . . . . . . . 43 6.2 Configuration ........................... 44 6.2.1 Configuration example . . . . . . . . . . . . . . . . . . 45 6.3 Functions ............................. 47 6.3.1 Channels and sending groups . . . . . . . . . . . . . . 48 6.3.2 Pyconnect commands . . . . . . . . . . . . . . . . . . . 49 6.4 Extending the software . . . . . . . . . . . . . . . . . . . . . . 50 7 Putting all together 53 7.1 Implementation.......................... 53 7.1.1 Features.......................... 55 8 Conclusions 59 Bibliography 63 List of Figures 63 ii Acknowledgments My most hearfelt thanks to my supervisors: Doctor Maria Alpuente who ha monitored constantly and patiently the writing of this thesis, Doctor Giorgio Levi who has encouraged me and given his support to its development abroad. Gisella for her help with English. I would also like to thank my parents for their financial support and - above all - their invaluable advice, and my sister who has proved to be a great friend. Finally, I thank all the friends who have helped me, directly or indirectly, to grow both professionally and as a person. Thanks to all. iii Chapter 1 Introduction The problem of data security is a fundamental aspect in any sector, and the growing ubiquity of mobile and distributed systems has accentuated the problem. Mobile code is software that is transferred between systems and executed on a local system without explicit installation by the recipient, even if it is delivered through an insecure network or retrieved from an untrusted source. During delivery, the code may be corrupted or a malicious cracker could change the code damaging the entire system. Potential problems can be summarized as problems related to security, allowing access to data or system resources which were not previously authorized, illegal or unlawful activities on the data, or functional incorrectness, that arises when the provided code fails to satisfy a necessary connection between its input and output. CodeCarrying Theory (CCT) [18, 19] is one of the technologies aimed at solving these problems. The idea of CCT is based on proof-based program synthesis, where a set of axioms that define functions are provided by the code producer together with suitable proofs guaranteeing that defined functions obey certain requirements. The form of the function-defining axioms is such that it is easy to extract executable code from them. Thus, all that has to be transmitted from the producer to the consumer is a theory (a set of axioms and theorems) and a set of proofs of the theorems. There is no need to transmit code explicitly. A basic implementation of the CCT methodology that uses a Fold/Unfold transformation framework for rewrite theories, and that reduces 1 1.1. PLAN OF THE THESIS. 1. Introduction the burden on the code producer is done in Rewriting logic [8]. Rewriting logic is efficiently implemented in the high-performance functional language Maude [10]. The purpose of this thesis is to extend and improve the framework for the CCT turning it into a stable and usable tool for Maude. The implementation is written in Maude itself, Python and some scripts in Bash. This thesis describe the general architecture of the system and the technical aspects that make it all modular and extensible. 1.1 Plan of the Thesis. The thesis is organized as follows: •In Chapter 2, we provide the necessary notation and preliminary definitions about the term rewriting formalism that will be used in this thesis. •In Chapter 3, we recall a Fold/Unfold based transformation framework for rewriting logic theories that we apply to implement the Code Carrying Theory (CCT) system. •In Chapter 4, we describe the overall structure of the Code Carrying Theory (CCT) system, and discusses how the framework described in Chapter 3 can be embedded into the system. •In Chapter 5, we analyze the security of the framework and analize a few examples of attacks that witness its weaknesses. Then we discuss how it is possible to prevent the attacks with the introduction of a suitable procedure for checking the certificates. •In Chapter 6, we describe the architecture of Pyconnect, a software system for connecting and communicating different processes through 2 1. Introduction 1.1. PLAN OF THE THESIS. only one system shell. •In Chapter 7, we describe the resulting refined framework for CCT extended for Certificate Checking, how it is assembled and how it works. •In Chapter 8, we present our conclusions and discuss some lines for future work. 3 3.2. Narrowing in Rewriting Logic functions, rules, equations, sorts, and algebraic laws (such as commutativity and associativity). When performing program transformation, we end up with a final program which is semantically equal to the initial one. During the transformation process, we need strategies (such as composition and tupling) which guide the application of the transformation rules and allow us to derive programs with improved performance, which can be done in a semi-automatic way. The process for obtaining a correct and efficient program can be split in two phases, which may be performed by different actors: the first phase is to write an initial maybe inefficient program whose correctness can be easily shown by hand or by automatic tools; in the second phase, the actor transforms the initial program by applying the rules of the framework to derive a more efficient one. We consider possibly non-confluent and non-terminating rewriting logic theories, and the operations for transforming these rewriting logic theories, with a strategy to restore completeness defined in [8], that preserves the rewriting logic semantics of the original theory. 3.2 Narrowing in Rewriting Logic Considering the rewrite relation →R/E introduced in Chapter 2, since Econgruence classes can be infinite, →R/E-reducibility is undecidable in general. One way to overcome this problem is to implement R/E-rewriting by a combination of rewriting using oriented equations and rules [20]. We define the relation →∆,B on TΣ(V) as follows: t→∆,B t0if there is a position p∈OΣ(t), l=rin ∆, and a substitution σsuch that t|p=Blσ and t0=t[rσ]p. The relation →R,B is similarly defined, and we define →R∪∆,B as →R,B ∪ →∆,B. The idea is to implement →R/E using →R∪∆,B. For this approach to be correct and complete, we need the following assumptions [16]. We assume the following properties on E= ∆ ∪B. (i) Bis non-erasing, and sort preserving. (ii) Bhas a finitary and complete unification algorithm, which implies that 10 3.2. Narrowing in Rewriting Logic B-matching is decidable, and ∆∪Bhas a complete (but not necessarily finite) unification algorithm. (iii) ∆ is sort decreasing, and confluent and terminating modulo B. (iv) →∆,B is coherent with B, i.e., ∀t1, t2, t3, we have that t1→+ ∆,B t2and that t1=Bt3implies ∃t4, t5such that t2→∗ ∆,B t4,t3→+ ∆,B t5, and t4=Et5. (v) →R,B is E-consistent with B, i.e., ∀t1, t2, t3, we have that t1→R,B t2 and that t1=Bt3implies ∃t4such that t3→R,B t4, and t2=Et4. (vi) →R,B is E-consistent with →∆,B, i.e., ∀t1, t2, t3, we have that t1→R,B t2 and that t1→∗ ∆,B t3implies ∃t4, t5such that t3→∗ ∆,B t4,t4→R,B t5, and t5=Et2. Narrowing [9],[12] generalizes term rewriting by allowing free variables in terms (as in logic programming) and by performing unification (at nonvariable positions) instead of matching in order to (nondeterministically) reduce a term. The narrowing mechanism has a number of important applications including automated proofs of termination, execution of functional-logic programming languages, partial evaluation, verification of cryptographic protocols and equational unification. The narrowing relation for rewriting logic theories is defined as follows [16]. Definition 1 (R∪∆, B-Narrowing) Let R= (Σ,∆∪B, R)be an ordersorted rewrite theory satisfying properties (i) - (vi) above. The R∪∆, Bnarrowing relation on TΣ(V)is defined as t;σ,p,R∪∆,B t0if there exist p∈ OΣ(t), a rule l→ror equation l=rin R∪∆, and σ, which is a Bunifier of t|pand lsuch that t0= (t[r]p)σ.t;σ,p,R∪∆,B t0is also called a R∪∆, B-narrowing step. Example 2 Consider the following rewrite theory (Σ,∆∪B, R) such that C={b, c, e},D1={a, d},D2={f}, ∆ = {a=b, d =e},R={f(x, f(y, b)) → d}where Bcontains the commutativity axiom for f. Then we can perform the narrowing step f(f(w, z), c);σ,Λ,R∪∆,B d, with σ={x/b, z/b}, since for 11 3.3. Transforming Rewrite Theories the commutativity of fwe have that f(f(w, z), c){z/b}=Bf(x, f(y, b)){x/c}.  When it is clear from the context, we omit R∪∆, B from the narrowing relation. Narrowing derivations are denoted by t0;∗ σtn, which is a shorthand for the sequence of narrowing steps t0;σ1,p1. . . ;σn,pntnwith σ=σn◦. . . ◦σ1(if n= 0 then σ=id). 3.3 Transforming Rewrite Theories In this section, we recall the fold/unfold transformation framework of PEPM 2010 by introducing the transformation rules over rewrite theories. Atransformation sequence of length kfor a rewrite theory (Σ,∆∪B, R) is a sequence R0,...,Ri,Ri+1,...,Rk,k≥0, where each Rj, 0 ≤j≤kis a rewrite theory, such that • R0= (Σ, E0, R0), with E0= (∆ ∪B) and R0=R. •For each 0 ≤j < i,Rj+1 = (Σ,∆j+1 ∪B, R0) is derived from Rjby an application of a transformation rule on the equation set ∆j. •For each i≤j < k,Rj+1 = (Σ, Ei, Rj+1) is derived from Rjby an application of a transformation rule on the rule set Rj. The transformation rules are Definition Introduction, Definition Elimination, Folding, Unfolding, and Abstraction, which are defined as follows. 3.3.1 Definition Introduction We can obtain program Rk+1 by adding to Rka set of new equations (resp. rules), defining a new symbol fcalled eureka. We consider equations (resp. rules) of the form f(ti) = ri(resp. f(ti)→ri), such that: (1) fis a function symbol which does not occur in the sequence R0,...,Rk and is declared by f:s1. . . sn→s[Ax], where s1, . . . , sn, s are sorts declared in R0and Ax are equational attributes. 12 3.3. Transforming Rewrite Theories (2) ti∈ TC(V), and Var(ti) = Var(ri), for all i— i.e., the equations/rules are non-erasing. (3) Every defined function symbol occurring in ribelongs to R0. (4) The set of new equations (resp. rules) are left linear, sufficiently complete and non overlapping. For rules we require also right linearity. In general, the main idea consists of introducing new auxiliary function symbols which are defined by means of a set of equations/rules whose bodies contain a subset of the functions that appear in the right-hand side of an equation/rule that appears in R0, whose definition is intended to be improved by subsequent transformation steps. The non overlapping property and the left-linearity ensure confluence of eurekas, which is needed to preserve the completeness of the fold operation and will be discussed later. Sufficient completeness is needed to ensure the completeness of unfolding and will be discussed later. Right-linearity on rules is needed to ensure narrowing completeness [16], and left-linearity is also needed to preserve the right-linearity of rules when doing folding. Consider, for instance, the folding of rule f(x)→g(x) using the (non left linear) eureka new(x, x)→g(x), which would produce a new rule f(x)→new(x, x), which is not right-linear. Note that, once a transformation is applied to a eureka, the obtained equation/rule is not considered to be a eureka anymore. As we will see later, this is important for the folding operation, since we can only fold non-eureka equations/rules using eureka ones. The non-erasing condition is a standard requirement that avoids the creation of equations/rules with extra-variables when performing folding steps. Consider, for instance, the folding of equation f(x) = g(x) using the (erasing) eureka new(x, y) = g(x), which would produce a new equation f(x) = new(x, y) containing an extra variable in its right-hand side (thus an illegal equation). 13 3.3. Transforming Rewrite Theories 3.3.2 Definition Elimination Let Rkbe the rewrite theory (Σk,∆k∪Bk, Rk). We can obtain program Rk+1 by deleting from program Rk, •all equations that define the functions f0, . . . , fn, say ∆f, such that f0, . . . , fndo not occur either in R0or in (Σk,(∆k\∆f)∪Bk, Rk). •all rules that define the functions f0, . . . , fn, say Rf, such that f0, . . . , fn do not occur either in R0or in (Σk,∆k∪Bk, Rk\Rf). Note that the deletion of the equations/rules that define a function fimplies that no function calls to fare allowed afterwards. However, subsequent transformation steps (in particular, folding steps) might introduce those deleted functions in the rhs’s of the equations/rules, thus producing inconsistencies in the resulting programs. To avoid this, we forbid any folding step after a definition elimination has been performed (this generally boils down to postpone all elimination steps to the end of the transformation sequence). 3.3.3 Folding Roughly speaking the Folding operation is the replacement of some piece of code by an equivalent function call. Let F∈ Rkbe an equation (the ”folded equation”) of the form (l=r), and let F0∈ Rj, 0 ≤j≤k, be an equation (the ”folding equation”) of the form (l0=r0), such that r|p=Bkr0σfor some position p∈OΣ(r) and substitution σ. Note that, since we transform the equations of an equational theory, we consider here the congruence relation =Bkmodulo the equational axioms Bk(assuming an empty equation set). This is because we cannot consider a congruence modulo an equational theory which is being modified. Moreover, the following conditions must be satisfied: (1) Fis not a eureka. (2) F0is a eureka. 14 3.3. Transforming Rewrite Theories (3) The substitution σis sort decreasing, i.e, if x∈ Vs, then xσ ∈ TΣ(V)s0 such that s0≤s. (4) Let l0=f(tn) and r|p=eand let f(tn) and ehave type sfand se, respectively; then sf≤se. Then, we can obtain program Rk+1 from program Rkby replacing Fwith the new equation (l=r[l0σ]p). Folding can be applied to rules whenever the transformation of the equational theory has been completed. To fold rules we proceed as follows. Let F∈ Rkbe a rule (the ”folded rule”) of the form (l→r), and let F0∈ Rj, 0≤j≤k, be a rule (the ”folding rule”) of the form (l0→r0), such that r|p=Ekr0σfor some position p∈OΣ(r) and substitution σ, fulfilling conditions (1) - (4) above. Then, we can obtain program Rk+1 from program Rk by replacing Fwith the new rule (l→r[l0σ]p). The need for conditions (1) and (2) is twofold. These conditions forbid self-folding, that is, a folding operation with F=F0, thus a rule with the same left and right-hand side cannot be produced, which may introduce infinite loops on derivations and destroy the correctness properties of the transformation system. These conditions also forbid the folding of a eureka, which is meaningless as illustrated in the following example. Example 3 Consider the following two rules: new →f(eureka) g→f(non-eureka) Without conditions (1) and (2), a folding of the eureka rule would be possible, obtaining the new rule (new →g), which is nothing more than a redefinition of the symbol new. Since transformation rules aim at optimizing the original program with the support of eurekas, a folding over a eureka is meaningless or even dangerous.  Finally, conditions (3) and (4) ensure the sort compatibility of both the applied substitutions and the term that is inserted into the folded equation/rule right-hand side. We can see an example of Folding operation. 15 3.3. Transforming Rewrite Theories Example 4 Consider the following rewrite theory: R= (ΣR,∅, R), where ΣRis the signature containing all the symbols of R and R: f(a, b)→g(a, b) f(x, y)→g(x, y) g(a, x)→a g(b, x)→b h(a)→a R0: f(a, b)→g(h(a), b) f(x, y)→g(x, y) g(a, x)→a g(b, x)→b h(a)→a We get program R0= (ΣR,∅, R0) from Rby applying a fold step to the rule f(a, b)→g(a, b) using the eureka h(a)→a. 3.3.4 Unfolding Unfolding is essentially the replacement of a call by its body, with appropriate substitutions. Let us introduce formally the Unfolding operation: Let R= (Σ,∆∪B, R) be a program and let Fbe an equation (resp. rule) of the form l=r(resp. l→r) in R. We obtain a new program from Rby replacing Fwith the set of equations (resp. rules) {lσ =r0|r;σ,∆,B r0is a ∆, B narrowing step} {lσ →r0|r;σ,R∪∆,B r0is a R∪∆, B narrowing step} Since we consider rewrite theories where defined symbols are allowed to be arbitrarily nested in left-hand sides of rules, rule unfolding may cause the loss of completeness for the transformed program w.r.t. the semantics of the original one. Let us illustrate this problem by means of an example. Example 5 Consider the following rewrite theory R= (ΣR,∅, R), where 16 3.3. Transforming Rewrite Theories ΣRis the signature containing all the symbols of Rand 1. 2. 3. 4. 5. R: g1(x)→x h(x)→0 h(g1(x)) →1 f(x)→g1(x) R0: g1(x)→x h(x)→0 h(g1(x)) →1 f(x)→x We get program R0= (ΣR,∅, R0) from Rby applying an unfolding step over rule 4 in R, through the narrowing step g1(x);εx. Term h(f(0)) can be rewritten in Rto the normal forms 0 or 1 by means of the rewrite sequences h(f(0)) →4h(g1(0)) →1h(0) →20, and h(f(0)) →4h(g1(0)) →3 1, respectively. The only possible rewrite sequences from h(f(0)) in R0are h(f(0)) →20, and h(f(0)) →5h(0) →20, thus we miss normal form 1. In fact, symbol g1is needed for rule 3 to be applied, and function fprovides that occurrence of g1needed to reach the normal form 1. However, the unfolding of rule 4 forces the occurrence of symbol g1to be evaluated, and, hence, that rewrite sequence is no longer available in R0. In [8] a procedure to restore completeness of the new program R0is proposed, together with a proof of soundness and a methodology for optimizing that procedure, which are outside the scope of this thesis. 3.3.5 Abstraction The set of rules presented so far constitute the core of our transformation system; however let us mention another useful rule, called Abstraction, which can be simulated in our settings by applying appropriate definition introduction and folding steps. This rule is usually required to implement tupling, and it consists of replacing, by a new function, multiple occurrences of the same expression ein the right-hand side of an equation/rule. For instance, consider the following equation double sum(x, y) = sum(sum(x, y), sum(x, y)) 17 3.4. Program Semantics and Correctness of the transformation system where e=sum(x, y). The equation can be transformed into the following pair of equations double sum(x, y) = ds aux(sum(x, y)) ds aux(z) = sum(z, z) These equations are generated from the original one by a definition introduction of the eureka ds aux and then by folding the original equation by means of the newly generated eureka. Note that the abstraction rule applies to equations or rules which are not right-linear, since the same expression eoccurs more than once in their rhs. Since we ask for rules to be right-linear for the completeness of the narrowing relation, we may think to use the abstraction rule to preprocess rewrite rules in order to try to make them right-linear. 3.4 Program Semantics and Correctness of the transformation system We now provide a definition of the considered program semantics. Definition 2 (Program Semantics) Given a program R= (Σ,∆∪B, R), the semantics of ground reducts of Ris the set gred(R) = {(t, s)|t∈ TΣ, t →∗ R∪∆,B s}. Let us also denote by gnf(R) (⊆gred(R)) the semantics of ground reducts in normal form, and by (t, s)∈gnf(E) the fact that sis the canonical form of tw.r.t. the equational theory E. The theoretical result for the transformation system based on the elementary rules introduced so far (definition introduction, definition elimination, unfolding, folding, and abstraction) are given in [8]. The main result is strong correctness of a transformation sequence, i.e., the semantics of the ground reducts gred( ) is preserved modulo the equational theory, as stated by Theorem 1. 18 3.4. Program Semantics and Correctness of the transformation system Theorem 1 Let (R0,...,Rk), k > 0, be a transformation sequence. Then, gnf(E0) =Bgnf(Ek), and for all t∈ TΣ0, if (t, s)∈gred(R0)then there exist s1,s2such that (t, s1)∈gred(Rk),(s, s2)∈gred(R0)and s1=E0s2. Viceversa, for all t∈ TΣ0, if (t, s)∈gred(Rk)then there exist s1,s2such that (t, s1)∈gred(R0),(s, s2)∈gred(Rk)and s1=E0s2. 19 4.2. Program Synthesis and CCT description dis a term of the following forms: •Definition Introduction Description: Intro(Operator Declaration, Equation Set) Intro(Operator Declaration, Rule Set) •Elimination Description: Elim(List of function symbols) •Unfolding Description: Unfold(Unfolded equation id, Unfold position) Unfold(Unfolded rule id, Unfold position) •Folding Description: Fold(Folding equation id, Folded equation id, Fold position) Fold(Folding rule id, Folded rule id, Fold position) Definition 4 (Certificate) Let (R0,...,Rk),k > 0, be a transformation sequence. The certificate associated with the transformation sequence (R0,...,Rk) is the ordered list of transformation rule descriptions C ≡ (d1, . . . , dk)associated with the transformation rules r1, . . . , rks.t. ∀i∈ {1, . . . , k},riis the transformation rule applied to Ri−1in order to obtain Ri. By applying the certificate provided by the Code Producer to the initial inefficient theory (R0), the Code Consumer obtains a new theory semantically equivalent to the first one but with improved performances (Rk). 4.2.2 Steps on new framework With the considered Certificates, so we can revisit the steps defined by the CCT methodology presented in Section 4.1.1 in order to work together in the new framework. The refined methodology consists only of 3 steps, which are illustrated in Figure 4.2, and summarized below. 26 4.2. Program Synthesis and CCT Fold/Unfold Transformation Optimized Code Requirement Definition (Rewrite Theory) Requirement Definition (Rewrite Theory) Code Synthesis Fold/Unfold Transformation Optimized Code Certificate CODE PRODUCER CODE CONSUMER Figure 4.2: Rewrite CCT Diagram 1. Code Consumer: Defining Requirements This step is similar to Step 1 of the basic CCT framework: the Code Consumer provides the requirements to the code producer in the form of a rewrite theory. The rewrite theory can be written in Maude, the high-level specification language that implements rewriting logic. 2. Code Producer: Defining New Functions This step resumes the steps [2,...,5]. The Code Producer uses the fold/unfold-based transformation system presented in Section 3.3 in order to obtain an efficient implementation of the specified functions. Subsequently, the producer will send only a Certificate Cdefined in Definition 4 to be used by the Code Consumer to derive the program. 3. Code Consumer: Code Extraction Once the Certificate is received, the code consumer can apply the transformation sequence, described in the Certificate, to the initial theory, and the final program is automatically obtained. The strong correctness 27 4.2. Program Synthesis and CCT of the transformation system ensures that the obtained program is correct w.r.t. the initial Consumer specifications., so the Code Consumer does not need to check extra proofs provided by the Code Producer. This covers Steps [6,...,9] of the basic methodology. 4.2.3 Case Study: a tail recursive function Let us provide an example that explains the overall mechanism described above. Assume the Code Consumer needs a function for computing the sum of the natural numbers in a list. The consumer specification is a rewrite theory which consists of the equational theory expressed by the following set of rules. op sum-list : NatList -> Nat . R1rl sum-list(nil) ⇒0 . R2rl sum-list(x xs) ⇒x + sum-list(xs) . The above rules defining the sum-list function can be transformed into a more efficient, tail-recursive structure by using the fold/unfold framework as follows. Introduce the following new eureka symbol sum-list-aux: op sum-list-aux : NatList Nat -> Nat . R3rl sum-list-aux(xs,x) ⇒x + sum-list(xs) . Apply the unfold operation over the eureka R3, we obtain the following new rules: R4rl sum-list-aux(nil, x) ⇒x + 0 . R5rl sum-list-aux(y ys, x) ⇒x + y + sum-list(ys) . 28 4.2. Program Synthesis and CCT Now, by folding rule R2 and R5 using the eureka R3, we obtain the final tail-recursive program. R1rl sum-list(nil) ⇒0 . R4rl sum-list-aux(nil,x) ⇒x + 0 . R6rl sum-list-aux(x xs,y) ⇒sum-list-aux(xs, x + y) . R7rl sum-list(x xs) ⇒sum-list-aux(xs, x) . The certificate Cis then as follows: ( Intro((op sum-list-aux :NatList Nat -> Nat.), (rl sum-list-aux(xs,x)⇒x+sum-list(xs).)), Unfold(R3,2), Fold(R3,R5,Λ), Fold(R3,R2,Λ) ) By applying now the certificate to the initial specification, the code consumer can efficiently obtain the required efficient implementation. 29 Chapter 5 Security attacks and extension of the framework In this Chapter, we analyze the security of the transformation framework for rewrite theories applied to CCT described in Chapter 4, and examine a few examples of attacks that witness the main weaknesses of the framework. Then, we discuss how it is possible to prevent the attacks by introducing a suitable procedure for checking the certificates. 5.1 Security Security is a fundamental aspect of every architecture based on a number of actors that exchange information among them. We have seen in Chapter 4 that the framework for CCT is based on two main actors (Code Consumer and Code Producer) and the data sent between them can be captured by a new malicious actor who could change them, and then cause incorrectness. For instance, the fold/unfold methodology in the CCT context is correct, because the code consumer does not start rewrites from any of the terms of the final theory but only on terms it had previously specified in the original theory, so if a code producer or some intruder in the middle introduces a new function foo, the code consumer never starts rewrites with foo. If we apply a correct certificate it is impossible to reach terms that carry malicious code 31 5.1. Security or improper operations. So if we want identify possible flaws, we need to look for certificates which do not satisfy the conditions of the transformations rules. In this section, we show a few examples which produce theories that are not correct or complete. Example 6 Consider the following rewrite theory R= (ΣR,∅, R), where X:: s∈ V and ΣRis the signature containing all the symbols of Rwith only one sort s, and 1. 2. 3. 4. 5. 6. R: f(a, a)→a f(b, c)→d a→b a→c g(X)→f(X, X) R0: f(a, a)→a f(b, c)→d a→b a→c g(a)→a We obtain program R0= (ΣR,∅, R0) from Rby applying an unfolding step over the rule g(X)→f(X, X)∈Rwhich is not right-linear, through the narrowing step f(X, X);X/a a. Let us consider term g(a). In the original program R,g(a) can rewrite to the normal form dby the rewrite sequence: g(a)→5f(a, a)→3f(b, a)→4f(b, c)→2d. In the transformed program R0, it is no longer possible from term g(a) to reach the term d, and, hence, the normal form dis lost.  As in the previous example, a Code Producer may send a Certificate with illicit operations which wen applied may result in a loss of code functionality. Terms no longer reachable may corrupt a whole system. Particularly they could make the system unstable or potentially attackable, if they had been designed for controlling critical conditions or processing security policies. This is only one possible scenario out of many, and perhaps less dangerous than others, the worst case being those configurations of certificates that lead out of the class of terms that were reached within the initial theory. That 32 5.1. Security is to say those certificates which cause a loss of correctness, as illustrated in the next example. When we presented the definition introduction operation, we said that eurekas have to be confluent in order to ensure the correctness of the fold operation. We now discuss this critical point by means of an example. Example 7 Consider the following rewrite theory R= (ΣR,∅, R), obtained from a previous theory R00 by introducing a fresh symbol m, where X:: s∈ V and ΣRis the signature containing all the symbols of Rwith only one sort sand R: f(a, b)→g(a, b) m(a)→a m(a)→b m(b)→a g(a, X)→a g(b, X)→b R0: f(a, b)→g(m(a), b) m(a)→a m(a)→b m(b)→a g(a, X)→a g(b, X)→b We get program R0= (ΣR,∅, R0) from Rby applying a folding step to the rule f(a, b)→g(a, b) using the eureka m(a)→a. It is easy to see that in R0we can reduce term f(a, b) to the normal forms aor b, while in Rwe can reach only the normal form a. The point is that in R, term f(a, b) can reduce only to g(a, b) while the fold operation introduces the possibility of rewriting it to g(b, b) cause the eureka defining mis not confluent. This leads to a new solution b, thus missing the correctness.  The above example clearly shows that the introduction of non-confluent functions, combined with the fold operation, leads to the achievement of new terms that would otherwise be previously unreachable, and therefore it extends the semantics of ground normal forms considered in the original theory. 33 5.1. Security 5.1.1 Hacking the certificate Although the code producer should ensure the correctness of the certificate and the framework for fold/unfold transformation ensures the correctness and completeness of the final program, there is no guarantee that the requirements of the transformation rules are met correctly. During delivery, the certicate might be corrupted, or a malicious hacker might change the code. Potential problems can be categorized as security problems (i.e., unauthorized access to data or system resources), safety problems (i.e., illegal operations), or functional incorrectness (i.e., the delivered code fails to satisfy a required relation between its input and output) If there is no automatic support, it is very easy for the code producer to make a mistake due to the large number of restrictions and preconditions, and it is even easier for an expert malicious hacker to intercept the certificate through an insecure network, modify it and resend to the code consumer. Consider the architecture discussed in Chapter 4 and summarized in Figure 4.2. In Figure 5.1 illustrate a possible attacking scenario, that we comment in the following example of a possible cracking of a certificate. Example 8 We now reuse the example discussed in Section 4.2.3 and we show what happens when changing the Certificate with functions which do no respect the preconditions. Remember that the consumer specification is a rewrite theory which is expressed by the following set of rules. op sum-list : NatList -> Nat . R1rl sum-list(nil) ⇒0 . R2rl sum-list(x xs) ⇒x + sum-list(xs) . The code producer improves the computational cost of this function and produces the certificate C: 34 5.1. Security Fold/Unfold Transformation Malicious Code Requirement Definition (Rewrite Theory) Requirement Definition (Rewrite Theory) Code Synthesis Fold/Unfold Transformation Optimized Code Certificate CODE PRODUCER CODE CONSUMER Certificate Manipulation Malicious Certificate Figure 5.1: Bad Certificate 35 Chapter 6 Pyconnect In this chapter, we provide the motivation that led us to implement Pyconnect. The reader will learn the functionalities, utility and the structure of the program. In addition we explain in detail how to configure it, and how to extend the source code and its classes in order to adapt at to any ad-hoc situations. 6.1 Description and Motivation Suppose you want to use a particular software to do a certain operation. Now assume that part of this result should be used by a consumer software. On Unix systems, the concept is well known and is widely used in a wide range of applications: we are obviously talking about the PIPE [13, 17]. If these software systems are developed in such a way as to fit with this concept, the solution is very simple: just call the execution of the two software systems by connecting them in a pipe which serially passes the output of the first one as the input for second one. In this way you can connect in a chain a potentially unlimited number of programs. What happens however, if these software systems are not written according to this paradigm, or the result of the second program must be reused by the first one that at the same time needs to maintain a state of consistency with its own data? 43 6.2. Configuration Obviously the solution of the PIPE is not ’appropriate. Pyconnect, developed in Python a programming language that allows you to work very quickly and integrate your systems more effectively with support for the object oriented paradigm [3, 2]. In our case we need to integrate two environments, in particular Maude [11] that runs the framework for the transformation of programs, and an extended version of Maude 2.3 with Ceta tree automata that is necessary for testing the sufficient completness [1], as due to incompatibility of versions, we are not able to integrate them directly within the maude language. Pyconnect is essentially an interactive pipe, which allows us, through a single interface, to transmit data from one or more sources to one or more destinations. Also it allows you to decide which data should be sent on time. Thanks to its modular design, it can be easily extended for ad-hoc solutions. With Pyconnect, we can integrate the two otherwise incompatible environments, and make invisible to the end user the process of transmitting data for the verification of the certificates described in Chapter 5. 6.2 Configuration Pyconnect manages communication of data, and it creates virtual channels that cannot be created at run-time, but must be declared in the configuration file, so that Pyconnect can create them at startup and manage at runtime. Pyconnect creates FIFOS [13] or named pipes which will be attached to the process. The names of those FIFOS must be specified in the configuration file and are part of the property of the channels created by Pyconnect . The configuration file ”pyconnect.config” is situated in the same folder of Pyconnect. We now see in detail its structure and its functionality.. All lines that begin with the character # are discarded because they are considered comments by Pyconnect. We have a group of four basic options that help to define the settings for a single channel: 44 6.2. Configuration •NAME: This variable is used by Pyconnect to recognize the name of the channel and to select it, for routing the data to and from it. The name of the channel must be unique; otherwise all channels with the same name in the environment of Pyconnect intercommunication are excluded. •PROC: This variable indicates the position in the file system of the process that must ’be started. •IN: This variable indicates the absolute path of the FIFO from which Pyconnect will read. To avoid confusion between those who will read or write, the names refer to Pyconnect, so assuming you create a channel with properties IN, the process attached to that channel must be written on this fifo. •OUT: This variable indicates the absolute path of the fifo on which Pyconnect will write the output data. To add a new channel it suffices to add into the configuration file a new group of the four variables listed above and their values. The lack of one of the variables in the introduction of a new channel will invalidate the configuration file. Finally, the variable DEFAULT indicate to Pyconnect which of the channels will be selected for communication by default. 6.2.1 Configuration example Here we can see a typical example of the configuration file, where there are two channels of communication with the first selected one as the default. 45 6.2. Configuration #simple configuration for Pyconnect DEFAULT = "maude" # maude channel # runs the framework NAME = "maude" # #the name of the proc not used PROC = "/usr/local/bin/maude" # uses a script to spawn maude like this # # maude < /tmp/readmeMaude > /tmp/writemeMaude # #the named pipe used for writing IN = "/tmp/wirtemeMaude" # #the named pipe used for reading OUT = "/tmp/readmeMaude" # maude-ceta channel # runs the sufficient completeness checker NAME = mceta" PROC = "/usr/local/bin/maude-ceta" # uses a script to spawn maude like this # # maude-ceta < /tmp/readmeMC > /tmp/writemeMC # #the named pipe used for writing IN = "/tmp/wirtemeMC" # #the named pipe used for reading OUT = "/tmp/readmeMC" 46 6.3. Functions 6.3 Functions Once your setup is done, Pyconnect is ready to run. The startup FIFOS specified in the configuration file are created and Pyconnetct waits for the connection of the process to them. When all processes are ready, Pyconnect shows you the shell ready for the communication with the channel specified by default. At this point, the user can enter input commands as if he were in the process. The commands will be passed directly to the selected process and the result will be shown on the screen. In Figure 6.1, you can see a session of Pyconnect with a channel of Maude. Figure 6.1: Pyconnect session 47 6.3. Functions To avoid that commands and controls of the processes overlap, Pyconnect uses a special escape sequence !@#$ This sequence is interpreted as the beginning of a command of Pyconnect and must be inserted every time you want to change a channel or modify a property of Pyconnect. 6.3.1 Channels and sending groups To understand how Pyconnect works and how to use it in an efficient way, we need to understand the concepts of channel and channel group. Pyconnect is an interactive pipe, but cannot select more than one input/output channels at the same time. Nevertheless this does not affect the ability to send data to other channels: the channel currently selected will have priority over others in that it will write the input of Pyconnect and all the data sent by the user or other connected processes will be sent to it. The other processes in those channels that are not selected will be in a state of running. Pyconnect does not interfere with their status, but only sends and receives data to be processed, so attention must be paid to synchronization problems among them. In Figure 6.2 you can see a schematic and detailed representation of the connections. The important thing to understand is that Pyconnect actually makes no difference between the user and a process. Also the processes can send commands to Pyconnect to change its state. It might be a good idea to organize a channel/process that supports the other processes, directs the control of the main execution and manages the flow of data when you need it. The communication primitives of Pyconnect are sufficient to direct traffic to a parent process. Pyconnect organizes channels in a group called sending group, and if the 48 6.3. Functions Pyconnect Process 1 CURRENT Process i Process NSend Process j Receive Process k IN OUT RECEIVE OUT CURRENT OUT CURRENT OUT RECEIVE IN IN OUT CURRENT OUT RECEIVE Figure 6.2: Pyconnect Connection Diagram channel is in this group, then it receives the data sent by Pyconnect. The prompt is always the list of channels that you are connected to and to which the data will be sent. 6.3.2 Pyconnect commands Let us summarize the commands of Pyconnect with their functionality. •!@#$ help : Prints help screen with the available commands. •!@#$ ls : Prints on screen a list of names of the channels configured by the system. 49 6.4. Extending the software •!@#$ select NAME: Selects a channel for communication. All informations will be sent to that channel. NAME refers to the name of the preset channel in the configuration file in the list (and available through the ls command). When you select a channel, its output will be sent to Pyconnect and will be sent in accordance with its status. •!@#$ send NAME : adds channel to channel send group. After this operation, the channel will receive an exact copy of the data sent to the selected communication channel. •!@#$ unsend NAME : opposite to the send command, clears the channel NAME from the channel send group. •!@#$ receive NAME : the currently selected channel receives data from channel. The input of an invalid command or a valid command with an invalid argument, does not change the system status. 6.4 Extending the software In this section, we discuss the main classes that make up Pyconnect. Pyconnect is written in Python because it is quite versatile and easy to extend. It is organized into a few classes that deal with all the work of routing data. In Figure 6.3, you can see the class diagram. The main class is RWproc, which calls the configuration file and initializes the fifos. It is the core of pyconnect, provides methods for high-level reading and writing in a channel, maintains the status and deals with parsing the command line, exchange operations and channel management. 50 6.4. Extending the software The class WriterGroup handles groups of channels and duplicates the input to and from these outwards. However, the important class that performs all the work of timing and data buffering is IStream class. This class contains the methods necessary to perform read and write operations to the stream and parseOut parseIn methods. They are invoked respectively by read and write, and take a string as input value and return a string as well. In the basic version of Pyconnect, these two methods do nothing but return the same string. However, if you extend Pyconnect for ad-hoc situations you can redefine these methods or extend the iStrem class by writing an ad-hoc parser for your own neceds. We should point out the abundance of tools for the Python language, including instruments that support regular expressions or others a bit more sophisticated such as bison, that can help you to develop your own solution. 51 Chapter 8 Conclusions In this dissertation, we investigated on some of the most recent and complex directions of research in computer science and we proposed some effective solutions. We extended a novel framework for Code Carrying Theory, which is fed with a methodology based on narrowing to perform fold/unfold program transformation. In order to achieve this goal, we made use of rule-based formalisms, such as rewriting logic, and narrowing to develop our system. The main aspect in which we concentrated our focus is the security and the interoperability of the framework. The core transformation rules of our CCT framework are folding, unfolding, definition introduction, and definition elimination. The correctness of the program transformation framework guarantees that the transformed program is equivalent to the initial one, and the program synthesis methodology can be effectively applied to CCT and significantly simplify the code producer and code consumer tasks. More precisely, the transformation process is represented as a compact sequence of applied transformation rules, and is delivered as a certificate to the code consumer. The distributed character of the considered systems has led us to the study of security aspects such as the software certification for secure the delivery of code, and we have shown that the code consumer cannot apply a certificate regardless of its contents, due to the possibility of certificate manipulation by a malicious actor that can attack the whole system. To obtain the desired final and improved program, 59 8. Conclusions the code consumer needs to check and apply the certificate to the initial requirements, which requires only modest computational resources. Future work related to the subject presented in this thesis includes experiments with optimizations to speed up the analysis, and automatize the code synthesis process. We implemented in a prototypical system the transformation framework and extended it with the infrastructure for certificate checking, which implements the complete CCT infrastructure, reducing the number of the steps and the burden of the code producer and the code consumer. So the code consumer which uses our framework can receive, check and apply a certificate to an initial theory in order to obtain the desired program, can detect and refuse bad certificates with a detailed report; and then avoid data corruption or attacks from malicious actors. We also plan to take advantage of the Pyconnect architecture, which allows us to integrate in our framework, in an easy way, some available Maude formal tools, to verify other relevant program properties such as termination and confluence of the initial equations set of the theory. Moreover, we can integrate an automated theorem prover for the verification of interested consumer properties. Such an extension is subject to future work. 60 Bibliography [1] http://maude.cs.uiuc.edu/tools/scc/, 2011. [2] Programming Python, 3rd Edition. O’Reilly, August 2006. [3] http://python.org, 2011. [4] Bouhoula A., Jouannaud J.P., and J. Meseguer. Specification and proof in membership equational logic. Theoretical Computer Science, 236(12):35–132, 2000. [5] M. Alpuente, M. Baggi, D. Ballis, and M. Falaschi. A fold/unfold framework for rewrite theories extended to cct, 2009. Submitted at: Workshop on Partial Evaluation and Program Manipulation (PEPM ’10). [6] M. Alpuente, M. Baggi, D. Ballis, and M. Falaschi. Maudeniccate program transformation system. Available at http://users.dimi.uniud.it/~michele.baggi/cct/, 2009. [7] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. [8] M. Baggi. Rule-based Methodologies for the Specification and Analysis of Complex Computing Systems Rule-based Methodologies for the Specification and Analysis of Complex Computing Systems. PhD thesis, Universidad Politecnica de Valencia, 2009. [9] M. Clavel, F. Dur´an, S. Eker, S. Escobar, P. Lincoln, N. Mart´ı-Oliet, J. Meseguer, and C. Talcott. Unification and narrowing in maude 2.4. In Ralf Treinen, editor, Rewriting Techniques and Applications, 20th 61 International Conference, RTA 2009, Bras´ılia, Brazil, 2009, Proceedings, volume 5595 of Lecture Notes in Computer Science, pages 380–390. Springer, 2009. [10] M. Clavel, F. Dur´an, S. Eker, P. Lincoln, N. Mart´ı-Oliet, J. Meseguer, and C. Talcott. The maude 2.0 system. In Robert Nieuwenhuis, editor, Rewriting Techniques and Applications (RTA 2003), number 2706 in Lecture Notes in Computer Science, pages 76–87. Springer-Verlag, 2003. [11] M. Clavel, F. Dur´an, S. Eker, P. Lincoln, N. Mart´ı-Oliet, J. Meseguer, and C. Talcott. All About Maude - A High-Performance Logical Framework. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2007. [12] M. Fay. First Order Unification in an Equational Theory. In Proc of 4th Int’l Conf. on Automated Deduction, pages 161–167, 1979. [13] GNU. Linux Programmer’s Manual, 2010. [14] Hitoshi Ohsaki Joe Hendrix and Jos´e Meseguer. Sufficient completeness checking with propositional tree automata. Technical report, University of Illinois, National Institute of Advanced Industrial Science and Technology, and PRESTO, Japan Science and Technology Agency. [15] J.W. Klop. Term Rewriting Systems. 1989. [16] J. Meseguer and P. Thati. Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher Order Symbolic Computation, 20(1-2):123–160, 2007. [17] Simone Piccardi. GaPiL Guida alla Programmazione in Linux. luglio 2010. [18] A. Vargun. Code-carrying theory. PhD thesis, Rensselaer Polytechnic Institute, Troy, NY, USA, 2006. Adviser-D.R., Musser. [19] A. Vargun and D.R. Musser. Code-carrying theory. In ACM symposium on Applied computing, pages 376–383, New York, NY, USA, 2008. ACM. [20] P. Viry. Rewriting: An effective model of concurrency. In Proceedings of the 6th International PARLE Conference on Parallel Architectures and Languages Europe, pages 648–660, London, UK, 1994. Springer-Verlag. List of Figures 4.1 Code Carrying Theory Diagram . . . . . . . . . . . . . . . . . 22 4.2 Rewrite CCT Diagram . . . . . . . . . . . . . . . . . . . . . . 27 5.1 BadCertificate .......................... 35 5.2 Certificate Checking . . . . . . . . . . . . . . . . . . . . . . . 38 6.1 Pyconnectsession......................... 47 6.2 Pyconnect Connection Diagram . . . . . . . . . . . . . . . . . 49 6.3 Pyconnect Classes Diagram . . . . . . . . . . . . . . . . . . . 52 7.1 Architecture of the framework . . . . . . . . . . . . . . . . . . 54 7.2 MetaMaudestCode . . . . . . . . . . . . . . . . . . . . . . . . 55 7.3 MetaMaudesCode Inclusion Modules Diagram . . . . . . . . . 57 65