NASA Journal of Innovations in Systems and Software Engineering manuscript No.(will be inserted by the editor)Deductive Veriﬁcation of Cryptographic SoftwareJose´ Bacelar Almeida · Manuel Barbosa · Jorge Sousa Pinto · Ba´rbara VieiraE-mail: (jba,mbb,jsp,barbarasv)@di.uminho.ptNovember 30, 2009Abstract We apply state-of-the art deductive veriﬁcationtools to check security-relevant properties of cryptographicsoftware, including safety, absence of error propagation, andcorrectness with respect to reference implementations. Wealso develop techniques to help us in our task, focusing onmethods oriented towards increased levels of automation, inscenarios where there are clear obvious limits to such au-tomation. These techniques allow us to integrate automaticproof tools with an interactive proof assistant, where the lat-ter is used off-line to prove once-and-for-all fundamentallemmas about properties of programs. The techniques devel-oped have independent interest for practical deductive veri-ﬁcation in general.Keywords Cryptographic algorithms; program veriﬁca-tion; program equivalence; self-composition.1 IntroductionSoftware implementations of cryptographic algorithms andprotocols are at the core of security functionality in many ITproducts. However, the development of this class of softwareproducts is understudied as a domain-speciﬁc niche in soft-ware engineering. The development of cryptographic soft-ware is clearly distinct from other areas of software engi-neering due to a combination of factors.– Firstly, cryptography is an inherently interdisciplinarysubject. The design and implementation of cryptogra-phic software draws on skills from mathematics, com-puter science and electrical engineering. The assumptionJ.B. Almeida ·M. Barbosa · J.S. Pinto · B. VieiraCCTC / Departamento de Informa´ticaUniversidade do MinhoCampus de Gualtar, 4710-Braga, Portugalthat such a rich body of research can be absorbed andapplied without error is tenuous for even the most expertsoftware engineer.– Secondly, security is notoriously difﬁcult to sell as a fea-ture in software products, even when clear risks such asidentity theft and fraud are evident. An important impli-cation of this fact is that security needs to be as close toinvisible as possible in terms of computational and com-munication load. As a result, it is critical that crypto-graphic software be optimised aggressively, without al-tering the security semantics.– Finally, typical software engineers develop systems fo-cused on desktop class processors within computers inour ofﬁces and homes. The special case of cryptographicsoftware is implemented on a much wider range of de-vices, from embedded processors with very limited com-putational power, memory and autonomy, to high-endservers, which demand high-performance and low-laten-cy. Not only must cryptographic software engineers un-derstand each platform and the related security require-ments, they must also optimise each algorithm with re-spect to each platform, since each one will have vastlydifferent performance characteristics.Program Veriﬁcation is the area of Formal Methods that at-tempts to check properties of software statically, with thehelp of an axiomatic semantics of the underlying program-ming language and a proof tool. Speciﬁcally, we are inter-ested in techniques based on Hoare logic [20], brought topractice through the use of contracts – speciﬁcations con-sisting of preconditions and postconditions, annotated intothe programs. In recent years veriﬁcation tools based on con-tracts have become more and more popular, as their scopeevolved from toy languages to very realistic fragments oflanguages like C[18,6], C# [4], or Java[23]. We will usethe expression deductive program veriﬁcation to distinguishthis approach from other ways of checking properties of pro-2grams, such as software model checking [2,19,22]. The goalof this paper is to apply deductive program veriﬁcation tech-niques to prove diverse properties of cryptographic software.Contributions. We describe results obtained in our explo-ration of existing veriﬁcation techniques and tools (used toconstruct high-assurance software implementations in otherdomains) to the concrete case of cryptographic software. Indoing so we have also developed techniques that are of in-dependent interest. Our contributions are the following.– We propose a composition-based methodology for prov-ing the functional equivalence of programs. This is in-spired by the self-composition technique [5] that can beused to prove information ﬂow properties of programs.Our methodology also enables self-composition proofs,although it targets the more general problem of provingthe correctness of concrete implementations with respectto speciﬁcations given as reference implementations– We employ natural invariants as a device to establisha correspondence between (annotation-level) axiomaticproperties of programs and (a formalisation of) their op-erational semantics. This device take us beyond the usualscope of contract-based veriﬁcation, enabling us to ob-tain automatic proofs relying on a battery of lemmaswhich are interactively proved once-and-for-all.– We show how natural invariants are useful for reasoningabout pairs of programs with similar control structures.In particular, this is a useful technique to enable programequivalence proofs in practice. It also allows for the au-tomation of the self-composition technique, which hasbeen identiﬁed as a major problem [32].– We show how these results enable us to use an off-the-shelf veriﬁcation tool to reason about functional correct-ness, safety properties, and security properties of a C im-plementation of the RC4 encryption scheme, included inthe well-known open-source library openSSL [29].CACE (Computer Aided Cryptography Engineering [8]) isan European Project that targets the lack of support cur-rently offered to cryptographic software engineers. The cen-tral objective of the project is the development of a tool-boxof domain-speciﬁc languages, compilers and libraries, thatsupports the production of high quality cryptographic soft-ware. The aim is that speciﬁc components within the tool-box will address particular software development problemsand processes; and combined use of the constituent tools isenabled by designed integration between their interfaces. Itis a three-year project that started in 2008.This article stems from CACE - Work Package 5, whichaims at adding formal methods technology to the tool-box,as a means to increase the degree of assurance than can beprovided by the development process.Organisation. Section 2 introduces the area of cryptograph-ic software implementation, and identiﬁes important secu-rity properties that deserve attention from a formal veriﬁ-cation point of view. We then discuss in Section 3 methodsto formalise and verify the validity of these properties us-ing a deductive veriﬁcation platform. Section 4 describes thedevelopment of an infrastructure to support the automationof the proposed approach, and Section 5 shows its appli-cation to a concrete case study: the veriﬁcation of the RC4openSSL implementation. We conclude the paper with a dis-cussion of related work in Section 6 and some concludingremarks in Section 7.2 A Catalogue of Software Properties2.1 Functional CorrectnessThe goal of functional correctness veriﬁcation is to establishthat a program performs according to some intended spec-iﬁcation. More precisely, that the input/output behaviour ofthe implementation matches that of the speciﬁcation. Thisis certainly the primary concern in program veriﬁcation andthe context in which the deductive approach has been mostwidely used. Verifying functional correctness within a de-ductive framework typically involves the following steps:1. annotating the source code with speciﬁcation contracts;2. adding invariant information for loops (and possibly alsovariants if total correctness is a concern);3. producing, with the help of a veriﬁcation condition gen-erator tool (VCGen), a set of veriﬁcation conditions; and4. discharging them (i.e. proving them) using an automaticor interactive prover.The critical points are steps 2 and 4, since the user needsto identify how certain properties are approximated duringthe loop execution – this is where most of the user activ-ity should be focused, since richer invariants will be harderto prove, but will simplify the veriﬁcation of the contract(by providing a richer set of hypotheses). Indeed, an activeresearch area is invariant synthesis, which attempts to au-tomatically generate these invariants by analysing the pro-gram. However, it should be kept in mind that the problemis inherently difﬁcult, even if certain approaches seem to be-have quite well for speciﬁc domains.Correctness with respect to a Reference Implementation.The standard scenario in deductive veriﬁcation is that spec-iﬁcations are written as contracts on the function and pro-cedure interfaces. This may involve properties of the outputvalues (typically written in ﬁrst-order logic), as well as rela-tions between input and output values.In this work we take an alternative route. We are inter-ested in verifying cryptographic software, whose speciﬁca-tions are typically given as operational descriptions (i.e. as3algorithms). This is the case, for example, in symmetric-keytechniques such as ciphers, message authentication codes,cryptographic hash functions, etc. When implementing sucha technique, the programmer will follow this description, butis free to improve the code, say by introducing optimisationsor internal reorganisations (e.g. to improve efﬁciency, main-tainability, or to satisfy non-functional security properties),as long as the input-output behaviour is the same as that pre-scribed by the speciﬁcation.To some extent, the speciﬁcation acts as a reference im-plementation: verifying functional correctness is reduced toproving program equivalence. Again, this is a difﬁcult (andundecidable) problem, although in this concrete applicationdomain we can rely on the fact that implementation andspeciﬁcation share most of their internal structure (since thelatter has been adopted as a model for the former). Indeed,the sort of equivalence proof required for cryptographic soft-ware corresponds to what is usually known in software en-gineering as code refactoring.2.2 Safety PropertiesDue to the inherent difﬁculty of the veriﬁcation of func-tional properties, less ambitious forms of veriﬁcation are of-ten used. A widespread veriﬁcation approach which aimsat increasing the level of assurance that can be placed onsoftware implementations is to conﬁne the analysis to a re-stricted class of properties that rule out the occurrence ofsome recognisable “bad things”. This is what is called asafety analysis, which often includes properties associatedwith common vulnerabilities arising from coding errors suchas de-referencing invalid pointers, accessing containers withinvalid indexes, calculation errors due to overﬂows, etc.The advantage of focusing on such simple properties isthat a signiﬁcant degree of automation can be achieved, min-imising user intervention and impact on development time.The resulting level of assurance, far from being absolute, isnevertheless sufﬁcient for a wide class of application sce-narios. In this work, we also brieﬂy review how a deductiveveriﬁcation tool can be used to perform this sort of analysis.2.3 Information Flow SecurityInformation ﬂow security refers to a class of security poli-cies that constrain the ways in which information can be ma-nipulated during program execution. These properties canbe formulated in terms of non-interference between high-conﬁdentiality input variables and low-conﬁdentiality out-put variables, and are usually veriﬁed using a special ex-tended type system [36,26,3]. A dual formulation permitscapturing security policies that constrain information ﬂowfrom non-trustworthy (or low-integrity) inputs, to trusted (orhigh-integrity) outputs. In Section 6 we provide an overviewof developments in this area related to the work in this paper.Consider the more common case of secure information-ﬂow that aims at preserving data conﬁdentiality. Informationmay ﬂow from high-security to low-security variables eitherdirectly via assignment instructions, or indirectly. The fol-lowing code from Terauchi and Aiken [32] computes in f1the nth Fibonacci number and then assigns a value to l thatdepends on the value of f1.f1 = 1; f2 = 0;while (n > 0) {f1 = f1 + f2;f2 = f1 - f2;n--; }if (f1 > k) l = 1; else l = 0;Let l be low security and n high security; then clearly thereis an indirect information leakage from n to l, since the as-signment l = 1 is guarded by a condition that depends onthe value of f1, and assignments to the latter variable areperformed inside a loop that is controlled by the high secu-rity condition n> 0. The program is thus insecure. If n werenot high security, the program would of course be secure.Type-based analyses would address the problem by trac-king assignments to low security variables. Observe, how-ever, that this fails to capture subtle situations where an ap-parently insecure program is in fact secure. If the last line ofthe program were changed toif (f1 > k) l = E1; else l = E2;where E1, E2 are two expressions that evaluate to the samevalue, then the program should be classiﬁed as high security,since there is no way to tell from the ﬁnal value of l anythingabout f1. Type-based analyses would typically fail to distin-guish this from the previous program: both would be conser-vatively classiﬁed as insecure. An alternative approach is todeﬁne a program as secure if different terminating execu-tions, starting from states that differ only in the values ofhigh-security variables, result in ﬁnal states that are equiv-alent with respect to the values of low-security variables.This approach, based on the language semantics, avoids theexcessively conservative behaviour of the previous method.More formally, let VH and VL denote respectively thesets of high-security and low-security variables of C, andV ′L = Vars(C) \ VH . We write (C,σ) ⇓ τ to denote the factthat when executed in state σ , C stops in state τ (states arefunctions mapping variables to values; ⇓ is the evaluationrelation in a big-step semantics of the underlying language).Then the program C is secure if for arbitrary states σ , τ ,σV ′L= τ ∧ (C,σ) ⇓ σ ′ ∧ (C,τ) ⇓ τ ′ =⇒ σ ′ VL= τ ′where σ X= τ denotes the fact that σ(x) = τ(x) for all x ∈ X ,i.e. σ and τ are X-indistinguishable.4Variants and Other Uses of Non-Interference. Non-interfer-ence has been recognised to be very strict in the sense thatit excludes any form of information ﬂow between high leveland low level security variables. Most of the times one needssome mechanism for declassifying data, allowing controlledﬂux of information between security levels. In Section 6 wepoint to some related work in this direction.We also point out that non-interference may be useful toexpress properties that are not directly concerned with se-curity, but are nevertheless useful in characterising speciﬁcaspects of cryptographic algorithms. As an example, con-sider the error-propagation property of stream ciphers suchas RC4, describing how they behave when used to transferdata over channels which may introduce transmission errors.The way in which the decryption process reﬂects a wrongciphertext symbol in the resulting plaintext is relevant: de-pending on the encryption scheme construction, a ciphertexterror may simply lead to a corresponding ﬂip in a plaintextsymbol, or it may affect a signiﬁcant number of subsequentsymbols. This property, sometimes called error propagation,is usually taken as a criterion for selecting ciphers for noisycommunication media, where the absence of error propaga-tion can greatly increase throughput. Note that error prop-agation can sometimes be seen as a desirable feature, as itampliﬁes errors that may be introduced maliciously, makingthem easier to detect.The intuition underlying the formalisation of error-prop-agation with non-interference is that secure information ﬂowcan be guaranteed by checking that arbitrary changes in low-integrity input variables cannot be detected by observinghigh-integrity output variables. We remark that the notionof a low-integrity input variable can be naturally associatedwith a transmission error over a communications channel.Hence, we map the ith possibly erroneous ciphertext sym-bol to a non-trusted low-integrity input (we are looking atthe decryption algorithm that, in the case of RC4, is iden-tical to the one used for encryption). The deﬁnition of non-interference can then conveniently be used to capture the ab-sence of error propagation. For this, we associate the outputplaintext symbols starting at position i+ 1 to trusted high-integrity outputs.More precisely, our formulation captures the followingidea: if an arbitrary change in the ith input ciphertext symbolcannot be observed in the output plaintext symbols follow-ing position i, this implies that the stream cipher does notintroduce error propagation in decryption.3 Proofs by CompositionIn this section we ﬁrst review self-composition, a techniquefor proving non-interference based on deductive veriﬁca-tion, and a generalisation (composition of two programs)that can be used to prove program equivalences. Our interestin reasoning about equivalence of programs is motivated bythe notion of “correctness with respect to a reference imple-mentation”, as explained in Section 2.The difﬁculties of applying self-composition in practiceare well-known, and they also apply to proofs of equiva-lence. In Section 3.3 we will introduce the notion of natu-ral invariant to overcome these difﬁculties. The techniqueestablishes a correspondence between program annotationsand an underlying formalisation of the operational semanticsof the programs. This allows us to prove (interactively) cer-tain fundamental lemmas that can be used to automaticallyprove properties based on the self-composition or composi-tion techniques.3.1 Self-CompositionThe operational deﬁnition of non-interference involves twoexecutions of the program but, using the self-compositiontechnique [5], it can be reformulated to consider a singleexecution (of a transformed program). Given some (deter-ministic) program C, let Cs be the program that is equal toC except that every variable x is renamed to a fresh variablexs. Non-interference can be formulated considering a sin-gle execution of the self-composed programC;Cs. Note thatany state σ of C;Cs can be partitioned into two states withdisjoint domains σ = σo ∪ σ s where dom(σo) = Vars(C)and dom(σ s) = {xs|x ∈ Vars(C)}. C is information-ﬂow se-cure if any terminating execution of the self-composed pro-gramC;Cs, starting from a state σ such that σo and σ s differonly in the values of high-security variables, results in a ﬁnalstate σ ′ such that σ ′o and σ ′s are equivalent with respect tothe values of low-security variables. This can be formulatedwithout referring explicitly to the state partition: if σ(x) =σ(xs) for all x ∈V ′L and (C;Cs,σ) ⇓ σ ′, then σ ′(x) = σ ′(xs)for all x ∈VL.Self-composition allows for a shift from an operationalsemantics-based to an axiomatic semantics-based deﬁnition,since the former can be written as the following Hoare logicpartial correctness speciﬁcation:{∧x∈V ′L x = xs}C;Cs{∧x∈VL x = xs}Difﬁculties of Applying Self-composition. The example ofSection 2.3 would result in the following self-composed pro-gram F ;Fs.f1 = 1; f2 = 0;while (n > 0) {f1 = f1 + f2; f2 = f1 - f2; n--;}if (f1 > k) l = 1; else l = 0;f1s = 1; f2s = 0;while (ns > 0) {5f1s = f1s + f2s; f2s = f1s - f2s; ns--;}if (f1s > ks) ls = 1; else ls = 0;This example was used in previous work by Terauchiand Aiken [32] to show the difﬁculties of mechanising self-composition using software model checkers. In order to usea VCGen, one would annotate the self-composed code withthe contract dictated by the following Hoare triple{n = ns∧ k = ks∧ l = ls} F ;Fs {l = ls}together with the obvious control invariants for each loop(regarding the minimum value of the variables n and ns).Some of the generated proof-obligations would not how-ever be discharged by an automatic prover. Admittedly, thecontrol invariants do not sufﬁciently describe what the loopsdo (in particular, the fact that they are calculating Fibonaccinumbers), and for this reason the post-condition cannot beproved, whether n==ns is included in the precondition (stat-ing that n is not considered high-security) or not. The ver-iﬁcation thus fails to recognize a secure program, even forsuch an apparently trivial example.3.2 Equivalence by CompositionThe above method can be extended to handle program equi-valence. Suppose we have two programs C1 and C2, andthat we are interested in proving their equivalence. Let V bethe set of variables occurring in both programs (we assumeboth use the same set of variables, otherwise we may letV = Vars(C1)∩Vars(C2)). The idea that we want to captureis that if the programs are executed from indistinguishablestates with respect toV , they terminate in states that are alsoindistinguishable. C1 and C2 will be deﬁned as equivalentif every execution of the composed program C1;Cs2, startingfrom a state in which the values of corresponding variablesare equal, terminates in a state with the same property. Thiscan be expressed as the following Hoare logic total correct-ness speciﬁcation:[∧x∈V x = xs]C1;Cs2 [∧x∈V x = xs]Weaker notions of equivalence can be handled by taking Vto be a subset of Vars(C1)∩ Vars(C2). In fact, we are notrestricted to equivalence relations – arbitrary relations canbe considered between the two partitions of the state:[R1(σ ,σ s)]C1;Cs2 [R2(σ ,σs)]where σ and σ s denote the state partitions associated withC1 and Cs2 respectively.The veriﬁcation of such assertions leads to similar difﬁ-culties to those already mentioned for self-composition: ingeneral there is no means to relate the outcomes of bothprograms, and automatic veriﬁcation fails. This was to beexpected, since establishing program equivalence is in gen-eral as undecidable problem.3.3 Natural InvariantsIn both scenarios identiﬁed above, the most evident difﬁ-culty of carrying out the veriﬁcation comes from the absenceof appropriate loop invariants. Of course, after ﬁnding theseloop invariants we still need to establish the intended proper-ties (ideally, with reasonable levels of automation). In whatfollows we propose a general approach to this problem. Inshort, it consists of the following steps:1. Extracting a speciﬁcation of each program from its re-lational semantics. We focus on the critical point of theveriﬁcation process, which is the construction of appro-priate loop invariants, and propose to construct them au-tomatically. The invariants we extract constitute the nat-ural speciﬁcation of each program, guaranteed to be sat-isﬁed by it. Each invariant is named and turned into anpredicate, which is then used to annotate the correspond-ing loop in the source code.2. Identifying and interactively proving additional facts in-volving the named invariant predicates. The critical ob-servation is that such lemmas correspond to basic refac-toring steps that are recurrently used in the developmentof cryptographic software. Their purpose is to relate thespeciﬁcations of the composed programs, capturing thenon-trivial parts of the proofs required for veriﬁcation.3. Augmenting the source ﬁle with the previous facts (writ-ten as lemmas), which have been justiﬁed once-and-for-all by interactive proofs. The availability of these lem-mas will allow automatic provers to carry out the ver-iﬁcation process, validating the veriﬁcation conditionsgenerated by a potentially large number of (self-) com-position proofs.We recall that we are primarily interested in tackling self-composition, as well as program equivalences when bothprograms share much of the underlying control structure.This makes it reasonable to assume that the user may easilyguide the interactive veriﬁcation process by providing hintsregarding the exploited code refactorings. This will allowthem to take advantage of the high degree of automationthat can be deployed to handle the remaining parts of theveriﬁcation process.Relational Speciﬁcation. For concreteness, we consider asimple While language with integer expressions and arrays.Its syntax is given by:P ::= {P} | skip | P1;P2|V := Eint | A[Eint ] := Eint| if (Ebool) then P1 else P2| while (Ebool) PEint ::= Constint | Eint op Eint | A[Eint ] op ∈ {+,−,∗,/, ...}Ebool ::= true | false | ¬Ebool | Ebool ∧Ebool | Ebool ∨Ebool| Eint opRel Eint opRel ∈ {=,<,>, ...}6We do not adopt any form of variable declaration. Instead,we consider a ﬁxed State type that keeps track of all thevariable values during the execution of the program. Integervariables are interpreted as (unbound) integers, and arraysas functions from integers to integers (no size / range check-ing). Array operations are axiomatised as usual:acc : (Z → Z)×Z → Zupd : (Z → Z)×Z×Z → (Z → Z)acc(upd(a,k,x),k) = xacc(upd(a,k′,x),k) = acc(a,k) if k = k′.The State type is deﬁned as the cartesian product of thecorresponding interpretation domains (each variable is asso-ciated to a particular position). We also consider an equiva-lence relation ≡ that captures equality on states. Integer andboolean expressions are interpreted in a particular state, thatis [[eInt ]] : State→ Z, [[eBool ]] : State→ B. We take the stan-dard deﬁnition for the big-step semantics of a program as itsnatural speciﬁcation. For states σ and σ ′ we deﬁne:specskip(σ ,σ ′) = σ ≡ σ ′spec{P}(σ ,σ ′) = specP(σ ,σ ′)specP1;P2 (σ ,σ′) = ∃σ ′′, specP1 (σ ,σ ′′)∧ specP2 (σ ′′,σ ′)specv:=E(σ ,σ ′) = σ ′ ≡ σ{v← [[E]](σ)}speca[E1]=E2 (σ ,σ′) = σ ′ ≡ σ{a← upd(a, [[E1]](σ), [[E2]](σ))}specif C then P1 else P2 (σ ,σ′) = ([[C]]σ ∧ specP1 (σ ,σ ′))∨(¬[[C]]σ ∧ specP2 (σ ,σ ′))specwhile (C) P(σ ,σ ′) = ∃n, loopnC,specP(σ ,σ ′)(σ ,σ′)∧¬[[C]](σ ′)where loopnC,R(σ ,σ′) is the inductively deﬁned relationloop0C,R(σ ,σ′)⇐= σ ≡ σ ′loopS(n)C,R (σ ,σ′)⇐= ∃σ ′′, loopnC,R(σ ,σ ′′)∧ [[C]](σ ′′)∧R(σ ′′,σ ′)The relation loopnC,R(σ ,σ′) denotes the loop speciﬁcationfor the body R under condition C. We call such a relationthe natural invariant for the loop (strictly speaking, this isin fact a relation that provides a natural choice for a loop’sinvariant). In this deﬁnition we have made explicit the it-eration rank (iteration count) in superscript – in fact, wewill see that it is often convenient to consider it explicitlyin the proofs. Nevertheless, when omitted, it should be con-sidered as existentially quantiﬁed. Also, we will omit sub-scripts (both in loop and spec) when the corresponding pro-grams are clear from the context.Expressiveness and Relative Completeness. Natural invari-ants capture the input-output relational semantics of pro-grams at the logical level. Naturally, they depend on a sufﬁ-ciently expressive assertion language, as it should allow forthe deﬁnition of new inductive relations. This correspondsessentially to Cook’s expressiveness criteria in his relativecompleteness result for Hoare Logic [12]. In fact, from nat-ural invariants we can easily recover the strongest liberalpredicate asslp(S,P) = {σ ′ | P(σ)∧ specS(σ ,σ ′)}An immediate consequence is that the veriﬁcation of an ar-bitrary Hoare triple could be conducted logically, as follows{P}S{Q} iff slp(S,P)⊇ Qiff ∀σσ ′, P(σ)∧ specS(σ ,σ ′)⇒ Q(σ ′).However, we note that the presence of loops immediatelyforces the use of full-ﬂedged inductive reasoning, compro-mising the aim of relying on automatic provers to conductsigniﬁcant parts of the proof. We will thus conﬁne such ageneral use of induction to general lemmas that will justifyspeciﬁc program transformations (refactorings).Verifying Trivial Equivalences. Let us focus for a momenton the veriﬁcation of the trivial equivalence by self-compo-sition (any program is equivalent to itself). By construction,spec enjoys the following properties.Lemma 1 Let R(σ ,σ ′) be a deterministic relation on states,and C a boolean condition. Then, loopC,R(σ ,σ ′) is deter-ministic whenever ¬[[C]](σ ′), i.e.loop synchronisation: ∀n1 n2 σ1 σ2 σ ′1 σ ′2,σ1 ≡ σ2∧ loopn1C,R(σ1,σ ′1)∧¬[[C]](σ ′1)∧ loopn2C,R(σ2,σ ′2)∧¬[[C]](σ ′2)=⇒ n1 = n2;loop determinism: ∀n σ1 σ2 σ ′1 σ ′2,σ1 ≡ σ2∧ loopnC,R(σ ,σ ′1)∧ loopnC,R(σ ,σ ′2) =⇒ σ ′1 ≡ σ ′2.Proof Both statements are proved by a simple induction (onmax(n1,n2) in the ﬁrst case, and n in the second). unionsqProposition 1 For every program fragment P and states σ1,σ2,σ ′1,σ′2,– spec is a morphism that preserves ≡. More precisely, ifσ1 ≡ σ2, σ ′1 ≡ σ ′2 and specP(σ1,σ ′1) then specP(σ2,σ ′2).– spec is deterministic. More precisely, if specP(σ ,σ ′1) andspecP(σ ,σ ′2) then σ′1 ≡ σ ′2.Proof By induction on the structure of P using Lemma 1.Lemma 1 enables a fully automatic proof of equivalenceof the self-composed program: it can be proved once-and-for-all and then included in the annotations provided to theveriﬁcation platform, allowing all other proof obligations tobe discharged. Indeed, our strategy for reasoning about mul-tiple executions of the same (or related) program(s) is basedon this observation: it is possible to identify a set of generallemmas that can be proven once-and-for-all, and that allowus to reason about self-composition assertions or to justifyinteresting refactorings (e.g. loop refactorings).7Self-composition Lemmas. The determinism property is notrelevant to reason about a non-interference property by self-composition: it merely states that the two instances of theprogram will produce the same outputs when all of their in-puts are equal. What is needed is a rephrasing of that prop-erty using an equality relation on low-security variables. Ifthe control structure of the program does not depend onhigh-security variables, the determinism property proof canbe carried over to non-interference lemmas. More explicitly,we recast each loop synchronisation lemma as follows∀n1 n2 σ1 σ2 σ ′1 σ ′2,πC(σ1)≡ πC(σ2)∧ loopn1C,R(σ1,σ ′1)∧¬[[C]](σ ′1)∧ loopn2C,R(σ2,σ ′2)∧¬[[C]](σ ′2) =⇒ n1 = n2where πC projects the fragment of the state that inﬂuencesthe control state (i.e. the loop conditions) – note that this canbe obtained by a simple (syntactical) dependency analysisthat collects all variables accessed by C and all variablesthat may interfere on the values of the latter through the loopbody. Then, a non-interference result for each loop followseasily from non-interference in its body:(∀σ1,σ2,σ ′1,σ ′2, σ1 ≡L σ2∧R(σ1,σ ′1)∧R(σ2,σ ′2)⇒ σ ′1 ≡L σ ′2)⇒ ∀σ1,σ2,σ ′1,σ ′2, σ1 ≡L σ2∧ loopn1C,R(σ1,σ ′1)∧¬[[C]](σ ′1)∧ loopn2C,R(σ2,σ ′2)∧¬[[C]](σ ′2)⇒ σ ′1 ≡L σ ′2We observe that proving non-interference for loop-free pro-grams by self-composition can be easily automated. The pre-condition for this lemma can be seen as an additional proof-obligation that must be veriﬁed.Justifying Loop Refactorings. The main difﬁculty of justify-ing code refactorings comes up when the refactorings affectloops. For the sake of presentation, we restrict our attentionto speciﬁcations obtained from single loops with loop-freebodies. That is, we consider natural invariants of the formloopC,spec(P)(σ ,σ ′) where P contains no loops. This case issufﬁcient to cover the program refactorings needed for es-tablishing correctness of the RC4 openSSL implementationaddressed in Section 5.The simplest loop refactoring that can be addressed us-ing our technique is loop unrolling, in which we detach in-stances of the loop body. This sort of transformation is justi-ﬁed by the following property that results from direct inver-sion of the deﬁnition of loop:∀n σ σ ′,loopS(n)C,R (σ ,σ′) =⇒∃σ ′′, loopnC,R(σ ,σ ′′)∧ [[C]](σ ′′)∧R(σ ′′,σ ′).or, in iterated form:∀n n′ σ σ ′,loopn(σ ,σ ′1)∧n′ < n =⇒∃σ ′′, loopn′ (σ ,σ ′′)∧ loopn−n′ (σ ′′,σ ′).Simple transformations like these are in fact better handleddirectly at the annotation level, rather than through explicitlemmas. Let us illustrate this by a small example that mim-ics an optimising transformation for the real-world examplepresented in Section 5. Consider the programi := 0;while (i N) then x := x + y else skip}else skipTo verify the equivalence between this implementation andthe original program it sufﬁces to identify the second loopinvariant in the second program as the following,loop2∗i(\old(x,y, i∗2),(x,y, i∗2))where \old(x) evaluates x in the pre-state of the loop, andloop(−) refers to the natural invariant of the loop in the ﬁrstprogram. By providing the invariant, we are making explicitthe correspondence between both loop executions. This kindof guidance is reasonable to expect from someone intendingto prove correctness of the target implementation.Alternatively, one could establish that both programs areequivalent using direct logical arguments, as will now beexplained. This would be the only option for more complexrefactorings.General Loop Fusions. To justify more signiﬁcant code re-factorings such as loop fusions (i.e. combining the bodies oftwo consecutive loops with the same control structure), weneed to rely on an explicit lemma. Consider the equivalencebetween two consecutive loops (loops 1 and 2) and one sin-gle fused loop (loop 3). This is reminiscent of another real-world code refactoring that will occur in our case-study inSection 5.Let us denote the natural invariants of these loops byloop1, loop2 and loop3, respectively. Since we assume that8all the loops share the same control structure (loop conditionand associated state), it is possible to prove mixed synchro-nisation lemmas such as∀n1 n2 σ1 σ2 σ ′1 σ ′2,πC(σ1)≡ πC(σ2)∧ loopn11 (σ1,σ ′1)∧¬[[C]](σ ′1)∧ loopn22 (σ2,σ ′2)∧¬[[C]](σ ′2) =⇒ n1 = n2.The proof is a straightforward generalisation of the singleloop version. Once this result has been established, one canprove the following main lemma that can be used to justifythe fusion refactoring:∀n σ1 σ2 σ ′1 σ ′′1 σ ′2,BodyFusion(body1,body2,body3)∧BodySwap(body1,body2)⇒σ1 ≡ σ2∧ loopn1(σ1,σ ′′1 )∧ loopn2(σ ′′1 ,σ ′1)∧ loopn3(σ2,σ ′2)=⇒ σ ′1 ≡ σ ′2,whereBodyFusion(R1,R2,R3) = ∀k, Rk3 ≡ (Rk2 ◦Rk1)BodySwap(R1,R2) = ∀kk′, k′ < k⇒ (Rk2 ◦Rk′1 )≡ (Rk′1 ◦Rk2)BodyFusion and BodySwap denote simple properties con-cerning the loop bodies which, as was the case with the self-composition lemmas, are all non-recursive and can thus beregarded as additional proof-obligations, easily dischargedby automatic provers.4 Veriﬁcation InfrastructureIn this work, we have used Frama-c [6], a tool for the staticanalysis of C programs that contains a multi-prover veriﬁ-cation condition generator [18]. We also employed a set ofproof tools that included the Coq proof assistant [33], andthe Simplify [15], Alt-Ergo [11], and Z3 [13] automatictheorem provers. C programs are annotated using the ANSI-C Speciﬁcation Language (ACSL [6]). Both Frama-c andACSL are work in progress; we have used the Lithium re-lease of Frama-c.Frama-c contains the gwhy graphical front-end that al-lows to monitor individual veriﬁcation conditions. This isparticularly useful when combined with the possibility ofexporting the conditions to various proof tools, which allowsusers to ﬁrst try discharging conditions with one or more au-tomatic provers, leaving the harder conditions to be studiedwith the help of an interactive proof assistant. An additionalfeature of Frama-c that we have found useful is the declara-tion of Lemmas. Like axioms, lemmas can be used to provegoals, but unlike axioms, which require no proof, lemmasoriginate themselves new goals. In the proofs we developed,it was often the case that once an appropriate lemma wasprovided (and proved interactively with Coq), all the veriﬁ-cation conditions could be automatically discharged.In this section we describe our use of these tools to sup-port the approach proposed in Section 3.4.1 Speciﬁcation GenerationThe ﬁrst step is to extract a relational speciﬁcation from theprogram code. This process proceeds by recursion on theprogram structure (Section 3.3) and produces the speciﬁca-tion as a logical formula.In practice, it is convenient to produce the intended for-mula in prenex-form. This is easily accommodated introduc-ing new fresh state variables in each elementary statement:specS1;S2;...;Sn (x1,x2) = ∃w0 . . .wn,w0 = x1∧w1 = PS1 (w0)∧ . . .∧wn = PSn (wn−1)∧ x2 = wnwhere PS(σ) is the atomic state transformation associatedwith statement S. The extracted speciﬁcation is then usedaccording to the proof goal factoring method described inthe previous section:1. It is encoded in the Coq proof assistant to provide thecontext in which the required speciﬁc lemmas can sub-sequently be proved interactively;2. It is included as ACSL loop invariant annotations in theC source code, to be fed to the Frama-c VCGen. Foreach loop speciﬁcation the corresponding invariant is in-cluded in the ACSL code. In this step the lemmas provedin step 1 are also provided as ACSL lemmas in the an-notated code, which should allow the remaining proofgoals to be discharged automatically.In the case study presented in Section 5 the speciﬁcation wasextracted by hand (see Appendix B), but we remark that theprocess is certainly amenable to mechanisation. Such a spec-iﬁcation extraction tool will be developed for the domain-speciﬁc crypto language CAO [17] as a deliverable of theCACE project.The Coq proofs mentioned in the ﬁrst step above areconstructed with support from a library that will now be de-scribed. Section 4.3 describes the second step above in moredetail.4.2 Coq LibraryA Coq library was developed to support the proof of lemmassuch as those introduced in Section 3. The library consistsof several layers:9– Frama-c interface, which includes the logical theory ex-ported by Frama-c and basic deﬁnitions/facts for rea-soning with the theory inside Coq;– Basic loop support, for basic treatment of loops (deriva-tion of determinism and synchronisation lemmas);– Refactoring lemmas: derivation of self-composition lem-mas and loop-fusion lemmas;– Demos and applications, which includes the RC4 exam-ple discussed in Section 5.We have made extensive use of Coq’s module system [9]in order to structure the development. As a rule, we embedeach lemma and respective proof in a functor parameterisedby basic facts it depends on. Concretely, we have deﬁned thefollowing.– BuildLoopFun: functor that builds the inductive deﬁ-nitions for loops and derives the corresponding deter-minism lemmas. It is parameterised by two modules de-scribing the loop state (the portion that affects the loopcondition and its complement) and the speciﬁcation ofthe loop body. These modules deﬁne the intended exten-sional equivalence on states and assert the determinismof the loop-body relation.– BuildSyncFun: functor that establishes the synchroni-sation of two loops that share the same boolean condi-tion. It is used, in particular, to derive a self-synchroni-sation lemma for each loop.– BuildSelfComp: generates and proves the self-compo-sition lemma. It is parameterised by the self-composi-tion property and the proof that the loop body satisﬁesthat property.– BuildFusionFun: generates and proves the fusion lem-ma for two loops. This accepts the description of threeloops (the loops to be fused and the resulting loop) to-gether with the following properties:– body-fusion property – asserts that the body of thethird loop behaves as the composition of the bodiesof the ﬁrst two loops;– body-shift property – asserts that iteration k of theﬁrst loop commutes with any of the ﬁrst k−1 itera-tions of the second loop.Note that all the results needed as inputs for the func-tors are non-recursive (they concern the loop body only) andcan be expected to be proved successfully by an automaticprover.4.3 Frama-c UsageFrama-c takes as input annotated C programs in the formof ACSL ﬁles. In particular, loop invariants are mandatoryfor the veriﬁcation to succeed. This means that in order toverify a property by composition, it is not enough to prop-erly construct the composed program and to specify the in-tended contract (pre- and post-conditions) – this would cer-tainly generate unprovable veriﬁcation conditions. It is alsorequired to complement the ACSL ﬁle with deﬁnitions andannotations. The following steps detail the procedure neededto perform the veriﬁcation:1. Including ACSL deﬁnitions corresponding to the induc-tive properties associated to each loop (see Section 4.1);2. For each loop speciﬁcation, annotating the program witha loop-invariant of the formInvloop(σ) = loopC,R(σ@Init,σ)where C and R are the loop’s condition and body, andσ@Init denotes the snapshot of the loop’s initial state(Frama-c supports this notion through the use of ex-plicit state labels in annotations).3. Augmenting the ACSL ﬁle with speciﬁc lemmas (provedin Coq with the support of the library of Section 4.2);4. Generating proof obligations with Frama-c;5. Using an automatic prover (e.g. Simplify) to discard thegenerated obligations.The choice of the required lemma is based on the speciﬁcproperty under scrutiny (e.g. a self-composition lemma fora non-interference property). We remark that this user-de-pendent choice is an important ingredient for the success ofthe veriﬁcation process. The goal of our method is to allowthe user to concentrate on this critical part of the veriﬁcationprocess by providing assistance in dealing with the remain-ing tasks, which are tedious but luckily prone to automation.5 Case Study: openSSL implementation of RC4RC4 is a symmetric cipher designed by Ron Rivest at RSAlabs in 1987. It is a proprietary algorithm, and its deﬁnitionwas never ofﬁcially released. Source code that allegedly im-plements the RC4 cipher was leaked on the Internet in 1994,and this is commonly known as ARC4 due to trademark re-strictions. In this work we will use the RC4 denominationto denote the deﬁnition adopted in literature [31]. RC4 iswidely used in commercial products, as it is included as oneof the recommended encryption schemes in standards suchas TLS, WEP and WPA. In particular, an implementation ofRC4 is provided in the pervasively used open-source libraryopenSSL, which we selected as the case study for this paper.In cryptographic terms, RC4 is a synchronous streamcipher, which means that it is structured as two indepen-dent blocks, as shown in Figure 1. The security of the RC4cipher resides in the strength of the key stream generator,which is initialized with a secret key SK. The key streamoutput is a byte sequence kt that approximates a perfectly10Key Stream GeneratorSKxyttktFig. 1 Block diagram of the RC4 cipherrandom bit string, and is independent of plaintext and ci-phertext (we adopt the most widely used version of RC4,implemented in openSSL, which operates over byte-sizedwords). The encryption operation consists simply of XOR-ing each plaintext byte xt with a fresh key stream byte kt . De-cryption operates in an identical way. The key stream gen-erator operates over a state which includes a permutation ta-ble S = (S[l])l=255l=0 of (unsigned) byte-sized values, and two(unsigned) byte-sized indices i and j. We denote the valuesof these variables at time t by St , it and jt . The state andoutput of the key stream generator at time t (for t ≥ 1) arecalculated according to the following recurrence, in whichall additions are carried out modulo 256.it = it−1 +1jt = jt−1 +St−1[it ]St [it ] = St−1[ jt ]St [ jt ] = St−1[it ]kt = St [St [it ]+St [ jt ]]The initial values of the indices i0 and j0 are set to 0, and theinitial value of the permutation table S0 is derived from thesecret key SK. The details of this initialisation are immate-rial for the purpose of this paper, as they are excluded fromthe analysis.We present in Appendix A the C implementation of RC4included in the openSSL open-source. The function receivesthe current state of the RC4 key stream generator (key), andtwo arrays whose length is provided in parameter len. Theﬁrst array contains the plaintext (indata), and the secondarray will be used to return the ciphertext (outdata). Thesame function can be used for decryption by providing theciphertext in the indata buffer. We note that this implemen-tation is much less readable than the concise description pro-vided above, as it has been optimised for speed using varioustricks, including macro inlining and loop unrolling. In therest of this section we brieﬂy present the veriﬁcation activi-ties performed on this case-study. Full details of it, includingall the annotated source ﬁles used, can be found in [1].5.1 Veriﬁcation of Safety PropertiesThe Frama-c VCGen allows users to perform a safety anal-ysis of C code, which may be run independently of func-tional veriﬁcation (see Section 2.2). This produces a specialclass of veriﬁcation conditions (called safety conditions) thatare not generated from contracts. Their validity implies thatthe program will execute safely with respect to a restrictedset of common programming errors that may result in incor-rect or unreliable implementations, or even with respect tosecurity vulnerabilities. These comprise memory safety, in-cluding the absence of buffer overﬂows, and also absence ofnumeric errors due to overﬂows in integer calculations.Note that, even though the proof obligations generatedfor the safety analysis do not result from explicit assertionsmade by the programmer, it is usually necessary to anno-tate the code with preconditions that permit justifying theproof goals. These preconditions limit the analysis to func-tion executions for which the caller has provided valid in-puts. For example, in RC4 one must assume that the indataand outdata arrays have a valid addressable range between0 and len-1 for the safety conditions to be valid. The inclu-sion of simple loop invariants to enable reasoning about theprogram state before, during and after each loop executionis also required. Finally, and given that cryptographic codetends to make use of some arithmetic operators that are notcommonly used in other application domains, we noted thatFrama-c lacked appropriate support in some cases, namelyfor bit-wise operators. To overcome this difﬁculty we addedsome very simple axioms to the annotated RC4 code.Running the Frama-c VCGen on the annotated sourcecode RC4 gave rise to 869 veriﬁcation conditions. All ofthese were automatically discharged using a set of automaticprovers that included Simplify, Alt-Ergo, and Z3.5.2 Error-propagation PropertyWe have used the self-composition technique described inSection 2.3 to verify whether the RC4 implementation inopenSSL indeed satisﬁes a property which is common to allsynchronous stream ciphers: the absence of error propaga-tion. Recall that this amounts to verifying that an erroneous(possibly tampered) input symbol, which will unavoidablyresult in a corresponding erroneous output symbol in thesame position, will not affect subsequent outputs. Formally,following the notation introduced in Section 2.3 that asso-ciates VH with the set of low-integrity input variables andVL with the set of high-integrity outputs, we have for somei ∈ [0, len[:VH = {indata[i]},VL = {outdata[ j] | i < j < len}.We have extracted natural invariants from the code andannotated the source ﬁle according to the procedure pre-sented in Section 4. The veriﬁcation with Frama-c resultedin the generation of 17 proof obligations, all of which were11unsigned char RC4NextKeySymbol(RC4_KEY *key) {unsigned char *d,x,y,tx,ty;x=key->x; y=key->y; d=key->data;x=((x+1)&0xff); tx=d[x];y=(tx+y)&0xff; d[x]=ty=d[y];d[y]=tx; key->x=x; key->y=y;return d[(tx+ty)&0xff];}void RC4(RC4_KEY *key, const unsigned long len,const unsigned char *indata,unsigned char *outdata) {int i=0;while(ix; y = key->y; d = key-> data;i=0;while(ix=x; key->y=y;}void RC4(RC4_KEY *key, const unsigned long len,const unsigned char *indata,unsigned char *outdata){unsigned char x,y,tx,ty, *d;int i;x = key->x; y = key->y; d = key-> data;i = (int)(len>>3L);while(i>0) {RC4LOOP(indata,outdata,0);RC4LOOP(indata,outdata,1);RC4LOOP(indata,outdata,2);RC4LOOP(indata,outdata,3);RC4LOOP(indata,outdata,4);RC4LOOP(indata,outdata,5);RC4LOOP(indata,outdata,6);RC4LOOP(indata,outdata,7);indata+=8; outdata+=8; i--;}i=(int)(len&0x07);while(i>0) {RC4LOOP(indata,outdata,i); i--; }key->x=x; key->y=y;}Fig. 4 RC4 refactoring steps 1 (top) and 2 (bottom).The ﬁnal refactoring steps, leading to the openssl ver-sion of RC4 in Appendix A, are introduced to achieve ad-ditional speed-ups. Firstly, pointer arithmetic is used to re-duce the range of indexing operations, and loop countingis inverted. Then, different control ﬂow constructions areapplied: all while loops are reformulated using the breakstatement to remove the ﬁnal backward jump, and if con-structions are introduced to detect termination cases. Equiv-alence checking for these low-level refactorings was per-formed directly in Frama-c.6 Related WorkA good survey of language-based information ﬂow securitycan be found in [30]. A good general view of self-composi-tion can be found in [10]. Information ﬂow policies wereﬁrst introduced by Denning et. al [14] and tend to be for-malised as noninterference properties. Information ﬂow typesystems, have been used to enforce noninterference in differ-ent contexts [36,27,26,34,35]. The main challenge in de-signing these systems is that they are often too conservativein practice, so that secure programs may be rejected. Leinoand Joshi [24] were the ﬁrst to propose a semantic approachto checking secure information ﬂow, with several desirablefeatures: a more precise characterisation of security; it ap-plies to all programming constructs whose semantics arewell-deﬁned; and it can be used to reason about indirect in-formation leakage through variations in program behaviour(e.g., whether or not the program terminates). An attempt tocapture this property in program logics using the Java Mod-elling Language (JML) [23] was presented by Warnier etal. [37], who proposed an algorithm, based on the strongestpostcondition calculus, that generates an annotated sourceﬁle with speciﬁcation patterns for conﬁdentiality in JML.Dufay et al. [16] have proposed an extension to JML toenforce non-interference through self-composition. This ex-tended annotation language allows for a simple deﬁnition ofnon-interference for Java programs. However, the generatedproof obligations are complex, which limits the general ap-plicability of the approach.Terauchi and Aiken [32] identiﬁed problems in the self-composition approach, arguing that automatic tools (soft-ware model checkers like SLAM [2] and BLAST [19]) arenot powerful enough to verify this property over programs ofrealistic size. To compensate for this, the authors propose aprogram transformation technique for an extended versionof the self-composition approach. Rather than replicatingthe original code, the renamed version is interleaved andpartially merged with it. Naumann[28] extended Terauchiand Aiken’s work to encompass heap objects, presented asystematic method to validate the transformations proposedin [32], and reported on the experience of using these tech-niques with the Spec# [4] and ESC/JAVA2 [21] tools.Natural Invariants provide an explicit rendition of pro-gram semantics. In [25] a similar encoding of program se-mantics in logical form can be found, which advocates theuse of second-order logic as appropriate to reason about pro-grams, since it allows to capture the inductive nature of theinput-output relations for iterative programs. To some ex-tent, our use of Coq’s higher-order logic may be seen as anendorsement of that view. However, we have made an ef-fort to combine the strengths of higher-order logic reasoningwith facilities provided by automatic ﬁrst-order provers.Relational Hoare Logic [7] has been used to prove thesoundness of program analyses and optimising transforma-tions. Its scope is thus similar to our proofs-by-compositionsetting. The main difference is the fact that we do not needto move away from traditional Hoare Logic, which allowsus to rely on standard available veriﬁcation tools.137 ConclusionWe have used an off-the-shelf veriﬁcation platform to checkseveral classes of properties of a real-world example of acryptographic software implementation: the widely used Cimplementation of the RC4 stream cipher available in theopenSSL library. Our results focus on three security-relevantproperties of this implementation, with increasing degreesof veriﬁcation complexity: (1) safety properties such as theabsence of numeric errors and memory safety; (2) absenceof error propagation formalised as non-interference; and (3)functional equivalence with respect to a reference imple-mentation.In more concrete terms, we have used Frama-c to provethat the RC4 implementation does not cause null pointer de-referencing exceptions, and always performs array accesseswith valid indices. In other words, the implementation issecure against buffer overﬂow attacks. Additionally, we de-monstrated that the limited ranges of numeric variables usedin the RC4 implementation are guaranteed not to introducecalculation errors for particular input values.An important property of stream ciphers such as RC4 istheir behaviour when a bit in the ciphertext is ﬂipped over acommunication channel. The behaviour of RC4 is commonto other synchronous ciphers: bit errors are not propagatedin any way, i.e. if a ciphertext bit is ﬂipped during transmis-sion, then only the corresponding plaintext bit is affected.We have formalised this property as a novel application ofthe non-interference concept, widely used in the formalisa-tion and veriﬁcation of secure information ﬂow properties,and subsequently proved that the RC4 implementation in-deed enjoys this property.Finally, we have also shown how the method introducedto prove non-interference can be applied to the more gen-eral case of equivalence proofs, to prove the correctness ofreal implementations with respect to reference implemen-tations. Cryptography is a prime candidate for equivalenceproofs, since speciﬁcations are usually given as referenceimplementations rather then using some high level model orlanguage. In concrete terms we have proved the equivalencebetween a reference implementation of RC4 and the realisticimplementation included in openSSL.Program equivalences are difﬁcult veriﬁcation challen-ges by nature, and automatic proof is of little help. Resort-ing to an interactive proof tool to conduct inductive proofsinvolving loops is inevitable. Our approach can be summedup as follows1. Program equivalences in general can be expressed asHoare triples using a composition technique that simu-lates the execution of two programs by a single program.Such triples can be written in an interface speciﬁcationlanguage like ACSL and fed to a standard VCGen likeFrama-c.2. Natural invariants are good candidates for establishingthe connection between the interface speciﬁcation lan-guage and the proof assistant: the ACSL speciﬁcationlanguage admits inductively deﬁned predicates, thus thenatural invariants annotated into the speciﬁcation ﬁles(fed to the VCGen) can make use of them, and lemmascan also be included in these ﬁles, to be (i) used by au-tomatic provers and (ii) exported to Coq for interactiveproof. These predicates / invariants (and some standardlemmas) can be generated mechanically. Note that sincethe typical ﬁrst-order prover does not support inductivepredicates, Frama-c will replace them by uninterpretedpredicates in the veriﬁcation conditions generated forthese provers (with axioms corresponding to the inter-actively proved properties). This allows to capture theprogram semantics through purely ﬁrst-order assertions.3. Concluding the veriﬁcation process is then a matter ofestablishing and proving interactively a small numberof adequate lemmas that concentrate the more creativeparts of the proofs required in the veriﬁcation process.To assist users in this more demanding task, we have de-veloped a dedicated Coq library. Once a lemma has beenproved in Coq and annotated into the composed speciﬁ-cation of the refactoring step, all the proof obligationsgenerated by Frama-c are discharged automatically.In addition to showing that deductive veriﬁcation meth-ods are increasingly more amenable to practical use withreasonable degrees of automation, our work answers someopen questions raised by previous work, which seemed toindicate that proofs by (self-)composition were not directlyapplicable in real-world situations. Our results are promis-ing in that we have been able to achieve our goal using onlyoff-the-shelf veriﬁcation tools.What is more, we believe that our technique has a highpotential for mechanisation. For instance, it is likely that theprocedure referred in Section 4.3 may itself be partially au-tomated. Speculating a bit, it is conceivable to extend ACSLwith constructs that mechanise some of the steps:\\@ lemma self_comp_lemma : \SelfCompLemma(loop1, ...);...loop1:\\@ loop invariant \natural_invariant(loop1);...An advantage of such an integration is that these annotationsmight trigger the generation of auxiliary proof obligations,such as those required by the functor that generates the self-composition lemma.Acknowledgements This work was partially supported by the Euro-pean Union under the FP7 project CACE (Project Number 216499),and by the FCT-funded RESCUE project (PTDC/EIA/65862/ 2006).14References1. Jose´ Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, andBa´rbara Vieira. Deductive veriﬁcation of cryptographic software.Technical Report DI-CCTC-09-03, CCTC, Univ. Minho, 2009.Available from http://cctc.uminho.pt/publications?year=2009.2. Thomas Ball and Sriram K. Rajamani. The SLAM project: debug-ging system software via static analysis. In POPL ’02: Proceed-ings of the 29th ACM SIGPLAN-SIGACT symposium on Princi-ples of programming languages, pages 1–3, New York, NY, USA,2002. ACM.3. Anindya Banerjee and David A. Naumann. Stack-based ac-cess control and secure information ﬂow. J. Funct. Program.,15(2):131–177, 2005.4. Mike Barnett, K. Rustan, M. Leino, and Wolfram Schulte. TheSpec# programming system: An overview. In Construction andAnalysis of Safe, Secure, and Interoperable Smart Devices, pages49–69. Springer, 2004.5. Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. Secure in-formation ﬂow by self-composition. In CSFW, pages 100–114.IEEE Computer Society, 2004.6. Patrick Baudin, Jean-Christophe Filliaˆtre, Claude Marche´, Ben-jamin Monate, Yannick Moy, and Virgile Prevosto. ACSL:ANSI/ISO C Specﬁcation Language. CEA LIST and INRIA, 2008.Preliminary design (version 1.4, December 12, 2008).7. Nick Benton. Simple relational correctness proofs for static anal-yses and program transformations. In Neil D. Jones and XavierLeroy, editors, POPL, pages 14–25. ACM, 2004.8. Computer Aided Cryptography Engineering. EU FP7. http://www.cace-project.eu/.9. Jacek Chrzaszcz. Implementation of modules in the Coq sys-tem. In David Basin and Burkhart Wolff, editors, Proceedings ofthe Theorem Proving in Higher Order Logics 16th InternationalConference, volume 2758 of LNCS, pages 270–286, Rome, Italy,September 2003. Springer.10. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. InCSF, pages 51–65. IEEE Computer Society, 2008.11. Sylvain Conchon, Evelyne Contejean, and Johannes Kanig. Ergo: a theorem prover for polymorphic ﬁrst-order logic modulo theo-ries, 2006.12. Stephen A. Cook. Soundness and completeness of an axiom sys-tem for program veriﬁcation. SIAM J. Comput., 7(1):70–90, 1978.13. Leonardo de Moura and Nikolaj Bjørner. Z3: An Efﬁcient SMTSolver, volume 4963/2008 of Lecture Notes in Computer Science,pages 337–340. Springer Berlin, April 2008.14. Dorothy E. Denning and Peter J. Denning. Certiﬁcation of pro-grams for secure information ﬂow. Commun. ACM, 20(7):504–513, 1977.15. David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theo-rem prover for program checking. J. ACM, 52(3):365–473, 2005.16. Guillaume Dufay, Amy Felty, and Stan Matwin. Privacy-sensitiveinformation ﬂow with JML. In Automated Deduction - CADE-20,pages 116–130. Springer Berlin / Heidelberg, August 2005.17. Dan Page (editor). CACE Deliverable D1.1: Complete CAOand qhasm speciﬁcations, 2009. Available from http://www.cace-project.eu.18. Jean-Christophe Filliaˆtre and Claude Marche´. TheWhy/Krakatoa/Caduceus platform for deductive programveriﬁcation. In Werner Damm and Holger Hermanns, editors,CAV, volume 4590 of Lecture Notes in Computer Science, pages173–177. Springer, 2007.19. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, andGre´goire Sutre. Lazy abstraction. In POPL ’02: Proceedingsof the 29th ACM SIGPLAN-SIGACT symposium on Principlesof programming languages, pages 58–70, New York, NY, USA,2002. ACM.20. C. A. R. Hoare. An axiomatic basis for computer programming.Communications of the ACM, 12:576–580, 1969.21. B. P. F. Jacobs, J. R. Kiniry, M. E. Warnier, Bart Jacobs, JosephKiniry, and Martijn Warnier. Java program veriﬁcation challenges.In FMCO 2002: Formal Methods for Component Objects, Pro-ceedings, volume 2852 of Lecture Notes in Computer Science,pages 202–219. Springer, 2003.22. Ranjit Jhala and Rupak Majumdar. Software model checking.ACM Computing Surveys, 41(4):1–54, 2009.23. Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, andBart Jacobs. JML (poster session): notations and tools support-ing detailed design in Java. In OOPSLA ’00: Addendum to the2000 proceedings of the conference on Object-oriented program-ming, systems, languages, and applications (Addendum), pages105–106, New York, NY, USA, 2000. ACM.24. K. Rustan M. Leino and Rajeev Joshi. A semantic approach tosecure information ﬂow. Lecture Notes in Computer Science,1422:254–271, 1998.25. Daniel Leivant. Logical and mathematical reasoning about imper-ative programs. In POPL, pages 132–140, 1985.26. Andrew C. Myers. Jﬂow: Practical mostly-static information ﬂowcontrol. In POPL, pages 228–241, 1999.27. Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. En-forcing robust declassiﬁcation and qualiﬁed robustness. Journalof Computer Security, 14(2):157–196, 2006.28. David A. Naumann. From coupling relations to mated invariantsfor checking information ﬂow. In Computer Security - ESORICS2006, volume 4189 of LNCS, pages 279– 296, 2006.29. The OpenSSL Project. http://www.openssl.org.30. A. Sabelfeld and A. Myers. Language-based information-ﬂow se-curity. IEEE Journal on Selected Areas in Communications, 21(1),2003.31. Bruce Schneier. Applied cryptography: protocols, algorithms, andsource code in C. Wiley, New York, 2nd edition, 1996.32. Tachio Terauchi and Alexander Aiken. Secure information ﬂowas a safety problem. In Chris Hankin and Igor Siveroni, editors,SAS, volume 3672 of Lecture Notes in Computer Science, pages352–367. Springer, 2005.33. The Coq Development Team. The Coq Proof Assistant ReferenceManual – Version V8.2, 2008. http://coq.inria.fr.34. Stephen Tse and Steve Zdancewic. A design for a security-typedlanguage with certiﬁcate-based declassiﬁcation. In Shmuel Sagiv,editor, ESOP, volume 3444 of Lecture Notes in Computer Science,pages 279–294. Springer, 2005.35. Jeffrey A. Vaughan and Steve Zdancewic. A cryptographic decen-tralized label model. In IEEE Symposium on Security and Privacy,pages 192–206. IEEE Computer Society, 2007.36. Dennis M. Volpano and Geoffrey Smith. A type-based approachto program security. In Michel Bidoit and Max Dauchet, editors,TAPSOFT, volume 1214 of Lecture Notes in Computer Science,pages 607–621. Springer, 1997.37. Martijn Warnier and Martijn Oostdijk. Non-interference in JML.Technical Report ICIS-R05034, Nijmegen Institute for Computingand Information Sciences, 2005.15A openSSL implementation of RC4typedef struct rc4_key_st{unsigned char x,y;unsigned char data[256];} RC4_KEY;void RC4(RC4_KEY *key,const unsigned long len,unsigned char *indata,unsigned char *outdata){register unsigned char *d;register unsigned char x,y,tx,ty;int i;x=key->x;y=key->y;d=key->data;#define LOOP(in,out) \x=((x+1)&0xff); \tx=d[x]; \y=((tx+y)&0xff); \d[x]=ty=d[y]; \d[y]=tx; \(out) = d[((tx+ty)&0xff)]^ (in);#define RC4_LOOP(a,b,i) LOOP(a[i],b[i])i=(int)(len>>3L);if (i){while(1){RC4_LOOP(indata,outdata,0);RC4_LOOP(indata,outdata,1);RC4_LOOP(indata,outdata,2);RC4_LOOP(indata,outdata,3);RC4_LOOP(indata,outdata,4);RC4_LOOP(indata,outdata,5);RC4_LOOP(indata,outdata,6);RC4_LOOP(indata,outdata,7);indata+=8;outdata+=8;if (--i == 0) break;}}i=(int)(len&0x07);if(i){while(1){RC4_LOOP(indata,outdata,0); if (--i == 0) break;RC4_LOOP(indata,outdata,1); if (--i == 0) break;RC4_LOOP(indata,outdata,2); if (--i == 0) break;RC4_LOOP(indata,outdata,3); if (--i == 0) break;RC4_LOOP(indata,outdata,4); if (--i == 0) break;RC4_LOOP(indata,outdata,5); if (--i == 0) break;RC4_LOOP(indata,outdata,6); if (--i == 0) break;}}key->x=x;key->y=y;}B ACSL loop speciﬁcation/*@ predicate eqAk{L1,L2}(integer k,@ unsigned char u1[],@ unsigned char u2[]) =@ \forall integer l;@ l!=k ==> \at(u1[l],L1)==\at(u2[l],L2);@*//*@ predicate eqA{L1,L2}(unsigned char u1[],@ unsigned char u2[]) =@ \forall integer l; \at(u1[l],L1)==\at(u2[l],L2);@*//*@ predicate RC4NextKeySymbol{L1,L2}(unsigned char *x,@ unsigned char *y,@ unsigned char d[],@ unsigned char k) =@ \exists unsigned char tx, unsigned char ty;@ \at(*x,L2) == ((\at(*x,L1) + 1) & 0xff) ==>@ tx == \at(d[\at(*x,L2)],L1) ==>@ \at(*y,L2) == ((tx+\at(*y,L1)) & 0xff) ==>@ ty == \at(d[\at(*y,L2)],L1) ==>@ \at(d[\at(*x,L2)],L2) == ty ==>@ \at(d[\at(*y,L2)],L2) == tx ==>@ k == (\at(d[(tx+ty)&0xff],L1);@*//** spec1{L,Here}((int)0,i,key,&(x),&(y),d);* Invariant for the first loop in Fig.3.*//*@@ inductive spec1{L1,L2}(integer i1,integer i2,@ unsigned char key[],@ unsigned char *x,@ unsigned char *y,@ unsigned char d[]) {@ case spec1_base{L} :@ \forall integer i1,integer i2,@ unsigned char key[],@ unsigned char *x,@ unsigned char *y,@ unsigned char d[];@ i1 == i2 ==> spec1{L,L}(i1,i2,key,x,y,d);@ case spec1_step{L1,L2,L3} :@ \forall integer i1,integer i2,integer i3,@ unsigned char key[],@ unsigned char *x,@ unsigned char *y,@ unsigned char d[],@ unsigned char k;@ spec1{L1,L2}(i1,i2,key,x,y,d) ==>@ eqAk{L2,L3}(i2,key,key) ==>@ RCNextSymbolKey{L2,L3}(x,y,d,k) ==>@ \at(key[i2],L3) == k ==>@ i3 == i2 +1 ==>@ spec1{L1,L3}(i1,i3,key,x,y,d);@ }@*/

Introduction Deductive Software Verification

Abstract

Extracted data

Introduction Deductive Software Verification

Abstract

Extracted data

Related items

Related items