A Translation from Typed Assembly Languages to Certified Assembly Programming

Zhaozhong Ni^{1} Zhong Shao^{2}

1 Microsoft Research, One Microsoft Way Redmond, WA 98052, U.S.A.

                  zhaozhong.ni@microsoft.com

2 Department of Computer Science,Yale University New Haven, CT 06520-8285, U.S.A.

                       shao@cs.yale.edu

Abstract. Typed assembly languages (TAL) and certified assembly programming (CAP) are two techniques for low-level verifications. TAL uses syntactic types and typing rules for program specification and reasoning, while CAP uses Hoare-style logic assertions and semantic subsumptions. They are suitable for different kinds of verification tasks. Previously, programs verified in either one of them can not interoperate freely with the other, making it hard to integrate them into a complete system. Moreover, the relationship between TAL and CAP lines of work has not been discussed extensively. In this paper, we do so by presenting a translation from a TAL language to a CAP language. The translation involves an intermediate step of a “semantic” TAL language. To better illustrate our key points, all three languages share a same untyped machine. Thus the shape of the source language is slightly different from the original TAL’s. Nevertheless, it supports polymorphic code, mutable reference, existential, and recursive types. The target language is an extension of XCAP, a recent CAP language, with support of logical recursive specifications and logical mutable reference, both require minimal changes to XCAP and its meta theory. Since we proved typing preservation for the translation, there is a clear path to link and interoperate well-typed programs from traditional certifying compilers with certified libraries by CAP-like systems.

1 Introduction

Proof-carrying code (PCC) [1] is a general framework that can, in principle, verify safety properties of arbitrary machine-language programs. Existing PCC systems [2–5], however, have focused on programs written in type-safe languages [6, 7] or variants of typed assembly languages (TAL) [8]. Type-based approaches are attractive because they facilitate automatic generation of the safety proofs (by using certifying compilers) and provide great support to modularity and higher-order language features. But they also suffer from several serious limitations. First, types are not expressive enough to specify sophisticated invariants commonly seen in the verification of low-level system software. Recent work on logic-based type systems [9–13] have made types more expressive but they still cannot specify advanced state invariants and assertions [14–16] definable in a general-purpose predicate logic with inductive definitions [17]. Second, type systems are too weak to prove advanced properties and program correctness, especially in the context of concurrent assembly code [15, 18]. Finally, different style languages often require different type systems, making it hard to reason about interoperability.

An alternative to type-based methods is to use Hoare logic [19, 20]—a widely applied technique in program verification. Hoare logic supports formal reasoning using very expressive assertions and inference rules from a general-purpose logic. In the context of foundational proof-carrying code (FPCC) [21, 22], the assertion language is often unified with the mechanized meta logic (following Gordon [23])—proofs for Hoare logic consequence relation and Hoare-style program derivations are explicitly written out in a proof assistant. For example, Touchstone PCC [24] used Hoare-style assertions to express complex program invariants. Appel et al [25, 26] used Hoare-style state predicates to construct a general semantic model for machine-level programs. Shao et al [22, 16, 18, 27] recently developed a certified assembly programming (CAP) framework that uses Hoare-style reasoning to verify low-level system libraries and general multi-threaded assembly programs.

TAL and CAP are suitable for different kinds of verification tasks. Previously, programs verified in either one of them can not interoperate freely with the other, making it hard to integrate them into a complete system. Moreover, the relationship between TAL and CAP lines of work has not been discussed extensively.

In this paper we compare the type-based and logic-based methods by presenting a type-preserving translation from a TAL language to a CAP langyage. The translation involves an intermediate step of a “semantic” TAL language. Our translation supports polymorphic code, mutable reference, existential, and recursive types. The target language is an extension of XCAP [27], a recent CAP language which supports embedded code pointers and impredicative polymorphisms. We added to XCAP the support of logical recursive specifications and logical mutable reference, both require minimal changes to XCAP and its meta theory, and call our new language XCAP+. Since we proved typing preservation for the translation from TAL to XCAP+, there is a clear path to link and interoperate well-typed programs from traditional certifying compilers with certified libraries by CAP-like systems.

We present the paper in the order of source language TAL (Sec 2), intermediate language STAL (Sec 3), and target language XCAP+ (Sec 4). Then we present the complete translation and the type-preservation properties (Sec 5). Finally we do some brief discussion and conclude (Sec 6).

2 Source Language: TAL

In this section we present a typed assembly language (TAL). To make the comparison easier, we build all languages in this paper on a common target machine. Throughout the paper, we also assume an underlying mechanized meta logic like

(Prop) p,q::= True| False | ¬p | p ∧ q | p ∨ q | p ⊃ q | ∀x:A.p | ∃x:A.p | ...

(Program) ℙ ::= (ℂ,𝕊,𝕀)
(State) 𝕊  ::= (ℍ,ℝ)
(Heap) ℍ ::= {l ⇝ w}^{∗}
(RegFile) ℝ ::= {r ⇝ w}^{∗}
(Register) r  ::= {rk}^{k∈{0...31}}
(Word,Labels) w,f,l ::= i (nat nums)

(CodeHeap) ℂ::= {f ⇝ 𝕀}^{∗}
(InstrSeq) 𝕀 ::= c;𝕀 | jdf | jmpr

(Command) c ::=

bgtir_{s},i,f | addi r_{d},r_{s},i
| add r_{d},r_{s},r_{t}
| movi r_{d},i | mov r_{d},r_{s}
| ldr_{d},r_{s}(i) | st r_{d}(i),r_{s}

Fig. 1. Syntax of target machine TM

if 𝕀 =  then (ℂ,(ℍ,ℝ),𝕀) ⟼→
jdf  (ℂ,(ℍ,ℝ),ℂ(f)) when f∈dom(ℂ)
jmpr  (ℂ,(ℍ,ℝ),ℂ(ℝ(r))) when ℝ(r)∈dom(ℂ)
bgtir_{s},i,f;𝕀′ (ℂ,(ℍ,ℝ),𝕀′) when ℝ(r_{s})≤i; (ℂ,(ℍ,ℝ),ℂ(f)) when ℝ(r_{s})>i
c;𝕀′  (ℂ,Nextc(ℍ,ℝ),𝕀′)
if c =  then Nextc(ℍ,ℝ) =
add r_{d},r_{s},r_{t} (ℍ,ℝ{r_{d}⇝ℝ(r_{s})+ℝ(r_{t})} )
mov r_{d},r_{s}  (ℍ,ℝ{r_{d}⇝ℝ(r_{s})})
movi r_{d},i (ℍ,ℝ{r_{d}⇝i})
ldr_{d},r_{s}(i) (ℍ,ℝ{r_{d}⇝ℍ(ℝ(r_{s})+i )}) when ℝ(r_{s})+i ∈ dom(ℍ)
st r_{d}(i),r_{s} (ℍ{ℝ(r_{d})+i⇝ℝ(r_{s})} ,ℝ) when ℝ(r_{d})+i ∈ dom(ℍ)

Fig. 2. Operational semantics of TM

2.1 Target Machine (TM)

We define the syntax and the operational semantics of the target abstract machine (TM) in Fig 1. A complete TM program consists of a code heap, a dynamic state component made up of the register file and data heap, and an instruction sequence. The instruction set is minimal but extensions are straightforward. To control the complexity of the paper, we ignore the allocation of memory. The register file is made up of 32 registers and the data heap can potentially be infinite. The operational semantics of this language (see Fig 2) should pose no surprise. Note that it is illegal to access undefined heap locations, or jump to a code label that does not exist; under both cases, the execution gets “stuck.”

2.2 Typed Assembly Language (TAL)

The TAL language presented here follows the principle of the original typed assembly languages [8]. However, due to the usage of an untyped raw machine, the shape of typing judgments and rules are slightly different.

Fig 3 presents the type definitions in TAL. Machine word is classified as of value type (τ) including integer, code, tuple, existential package, and recursive data structures. A code heap specification (Ψ) is a partial environment that maps a code label to a “precondition” type ([Δ].Γ) for its corresponding code block. Here Δ is a type variable environment and Γ is a register file type which specifies the type for each register.

Ψ ⊢{[Δ].Γ}ℙ (Well-formed Program)

\begin{aligned}⊢ ℂ:Ψ & Ψ ⊢ 𝕊:[Δ].Γ & Ψ ⊢\{[Δ].Γ\}𝕀 \\ & Ψ ⊢\{[Δ].Γ\}(ℂ,𝕊,𝕀) \end{aligned} (prog)

⊢ ℂ:Ψ (Well-formed Code Heap)

\begin{matrix}Ψ ⊢\{Ψ(f) \}ℂ(f)  ∀f∈dom(Ψ) \\ ⊢ ℂ:Ψ \end{matrix} (cdhp)

(CdHpSpec) Ψ::= {f ⇝ [Δ].Γ}^{∗}
(RfileTy) Γ ::= {r ⇝ τ}^{∗}
(TyVarEnv) Δ ::= · | α,Δ
(WordTy) τ ::= α | int| code [Δ].Γ ; | ⟨τ_{1},...,τ_{n}⟩| ∃α. τ ; | μα.τ

(DtHpSpec) Φ ::= {l ⇝ τ}^{∗}

Ψ ⊢{[Δ].Γ}𝕀 (Well-formed Instruction Sequence)

⊢{Γ}c{Γ′}  Ψ ⊢{[Δ].Γ′}𝕀 c∈{add,mov,movi,ld,st} Ψ ⊢{[Δ].Γ}c;𝕀 (seq)  f∈dom(Ψ) Ψ ⊢{[Δ].Γ{r_{d}⇝code Ψ(f) }}𝕀 Ψ ⊢{[Δ].Γ}movi r_{d},f;𝕀 (movf)

f∈dom(Ψ)  ⊢ [Δ].Γ ≤ Ψ(f) Ψ ⊢{[Δ].Γ}jdf (jd)  Γ(r) =code [Δ′].Γ′ ⊢ [Δ].Γ ≤ [Δ′].Γ′ Ψ ⊢{[Δ].Γ}jmpr (jmp)

f∈dom(Ψ)  Γ(r_{s}) =int Ψ ⊢\{[Δ].Γ\}𝕀  ⊢ [Δ].Γ ≤ Ψ(f) Ψ ⊢\{[Δ].Γ\}bgtir_{s},i,f;𝕀 (bgti)  \begin{matrix}⊢ [Δ].Γ ≤ [Δ′].Γ′ & Ψ ⊢\{[Δ′].Γ′\}𝕀 \\ Ψ ⊢\{[Δ].Γ\}𝕀 \end{matrix} (weaken)

Fig. 3. Type definitions and top-level static semantics of TAL

Similarily, a data heap specification (Φ) is a partial environment that maps from a data label to a value type for its corresponding heap cell.

The top-level semantic rules of TAL are also presented in Fig 3. A program is wellformed if each of its components is. For a code heap to be well-formed, each block in it must be well-formed. The intuition behind well-formed instruction sequence judgment is that if the state satisfies the precondition [Δ].Γ, then executing 𝕀 is safe with respect to Ψ. Weakening is allowed to turn one precondition into another provided that they satisfy the subtyping relation. A instruction sequence c;𝕀 is safe if one can find another register file type which serves as both the post-condition of c and the precondition of 𝕀. A direct jump is safe if the current precondition implies the precondition of the target code block specified in Ψ. An indirect jump is safe when the target register is of a code type with a weaker precondition. Constant code labels can be moved into registers.

The remaining typing rules for TAL is presented in Fig 4. Valid subtypings include reducing the registers, instantiation of code type, packing, unpacking, folding, and unfolding. For simple instructions, their pre- and post-conditions do not involve change of type variable environment, thus we only specify the register file types before and after their execution. The well-formed state rule instantiates the current type variable environment and requires a current data heap specification to be supplied and checked. Other judgments and rules are standard and straight-forward.

⊢ [Δ].Γ ≤ [Δ′].Γ′ (Subtyping)

\begin{matrix}Δ ⊇ Δ′ ∀ r ∈ dom(Γ′) \\ Γ(r) =Γ′(r) Δ′ ⊢ Γ′(r) \end{matrix} ; ⊢ [Δ].Γ ≤ [Δ′].Γ′ (subt)  Γ(r) =code [α,Δ′].Γ′ Δ ⊢ τ′ ⊢ [Δ].Γ ≤ [Δ].Γ\{r:code [Δ′].Γ′[τ′/α]\} (tapp)

\begin{matrix}Γ(r) =τ[τ′/α] Δ ⊢ τ′ \\ ⊢ [Δ].Γ ≤ [Δ].Γ\{r:∃α. τ\} \end{matrix} (pack)  \begin{matrix}Γ(r) =∃α. τ \\ ⊢ [Δ].Γ ≤ [α,Δ].Γ\{r:τ\} \end{matrix} (unpack)

\begin{matrix}Γ(r) =τ[μα.τ/α] \\ ⊢ [Δ].Γ ≤ [Δ].Γ\{r:μα.τ\} \end{matrix} (fold)  \begin{matrix}Γ(r) =μα.τ \\ ⊢ [Δ].Γ ≤ [Δ].Γ\{r:τ[μα.τ/α]\} \end{matrix} (unfold)

⊢{Γ}c{Γ′} (Well-formed Instruction)

Γ(r_{s}) = int ⊢{Γ}addi r_{d},r_{s},i{Γ{r_{d}:int}} (addi)  Γ(r_{s}) = Γ(r_{t}) = int ⊢{Γ}add r_{d},r_{s},r_{t}{Γ{r_{d}:int}} (add)

⊢\{Γ\}movi r_{d},w\{Γ\{r_{d}:int\}\} (movi)  \begin{matrix}Γ(r_{s}) = τ \\ ⊢\{Γ\}mov r_{d},r_{s}\{Γ\{r_{d}:τ\}\} \end{matrix} (mov)

Γ(r_{s}) =⟨τ_{1},...,τ_{w+1} ,...,τ_{n}⟩ ⊢{Γ}ldr_{d},r_{s}(w){Γ{r_{d}:τ_{w+1} }} (ld)  Γ(r_{d}) =⟨τ_{1},...,τ_{w+1} ,...,τ_{n}⟩ Γ(r_{s}) =τ_{w+1} ⊢{Γ}st r_{d}(w),r_{s}{Γ} (st)

Δ ⊢ τ Ψ ⊢ 𝕊:[Δ].Γ Ψ ⊢ ℍ:Φ Ψ;Φ ⊢ ℝ:Γ Ψ;Φ ⊢ w:τ

(Well-formed Type, State, Heap, Register file, and Word)

\begin{matrix}F T V(τ)⊆Δ \\ Δ ⊢ τ \end{matrix} (type)  \begin{matrix}· ⊢ τ_{i} ∀ i Ψ ⊢ ℍ:Φ Ψ;Φ ⊢ ℝ:Γ[τ_{1},...,τ_{n}/α_{1},...,α_{n} ] \\ Ψ ⊢ (ℍ,ℝ):[α_{1},...,α_{n}].Γ \end{matrix} (state)

\begin{matrix}Ψ;Φ ⊢ ℍ(l):Φ(l) & ∀ l∈dom(Φ) \\ Ψ ⊢ ℍ:Φ \end{matrix} (heap)  \begin{matrix}Ψ;Φ ⊢ ℝ(r):Γ(r) & ∀ r∈dom(Γ) \\ Ψ;Φ ⊢ ℝ:Γ \end{matrix} (rfile)

Ψ;Φ ⊢ w:int (int)  f∈dom(Ψ) Ψ;Φ ⊢ f:code Ψ(f) (code)  · ⊢ τ′ Ψ;Φ ⊢ f:code [α,Δ].Γ Ψ;Φ ⊢ f:code [Δ].Γ[τ′/α] (poly)

\begin{matrix}Φ(l+i−1 ) =τ_{i} ∀ i \\ Ψ;Φ ⊢ l:⟨τ_{1},...,τ_{n}⟩ \end{matrix} (tup) \begin{matrix}· ⊢ τ′ & Ψ;Φ ⊢ w:τ[τ′/α] \\ Ψ;Φ ⊢ w:∃α. τ \end{matrix} (ext)  \begin{matrix}Ψ;Φ ⊢ w:τ[μα.τ/α] \\ Ψ;Φ ⊢ w:μα.τ \end{matrix} (rec)

Fig. 4. Static semantics of TAL (continued)

The soundness theorem guarantees that given a well-formed program, the machine will never get stuck. It is proved following the syntactic approach of proving type soundness [28]. We also list a few key lemmas below.

Theorem 1 (TAL Soundness). If Ψ ⊢{[Δ].Γ}ℙ , then for all natural number n, there exists a program ℙ′such that ℙ ⟼→^{n} ℙ′.

Lemma 1 (State Weakening). If Ψ ⊢ 𝕊:[Δ].Γ and ⊢ [Δ].Γ ≤ [Δ′].Γ′ then Ψ ⊢ 𝕊:[Δ′].Γ′.

Lemma 2 (Instruction Typing). If Ψ ⊢ 𝕊:[Δ].Γ and ⊢ {Γ}c{Γ′} then Ψ ⊢ Nextc(𝕊):[Δ].Γ′ .

3 A “Semantic” TAL Language

Instead of doing translation from TAL to CAP directly, we create a new “Semantic” TAL language (STAL) to serve as an intermediate step between them. Let us revisit the static semantics of TAL in Figure 4 and the lemmas used in TAL soundness proof.

First look at the set of subtyping rules between preconditions (⊢ [Δ].Γ ≤ [Δ′].Γ′). If we also look at the State Weakening lemma (Lemma 1) in TAL soundness proof, it is easy to see that all of those syntactic rules are just used for the meta implication between the two state typings in the soundness proof. Given a mechanized meta logic, we can replace these rules with a single one,

\begin{matrix}Ψ ⊢ 𝕊:[Δ].Γ ⊃ Ψ ⊢ 𝕊:[Δ′].Γ′  ∀ 𝕊,Ψ \\ ⊢ [Δ].Γ ≤ [Δ′].Γ′ \end{matrix} (subt)

which explicitly requests the meta implications between two state typing. By doing so, not only did we remove the fixed syntactic subtyping rules from TAL, but the State Weakening lemma is no longer part of the soundness proof. More importantly, the subtyping between preconditions is no longer limited to the built-in rules. Any valid implication relation between state typing is allowed. This is much more flexible and powerful.

Now let us look at the set of instruction typing rules (⊢ {Γ}c{Γ′}). Also look at the Instruction Typing lemma (Lemma 2) in TAL soundness proof. Again all these syntactic rules are just used for the meta implication between two state typings in the soundness proof. (The difference this time is that the two states are now different and are states before and after the execution of an instruction.) Applying our trick again, we can replace these rules with a single one,

\begin{matrix}Ψ ⊢ 𝕊:[Δ].Γ ⊃ Ψ ⊢ Nextc(𝕊):[Δ].Γ′ ∀ 𝕊,Ψ \\ ⊢ \{Γ\}c\{Γ′\} \end{matrix} (instr) .

We also successfully removed the fixed syntactic instruction typing rules as well as he Instruction Typing lemma from TAL. The new form of instruction typing is much more flexible and powerful.

Of course, in composing the actual meta proof supplied to the new SUBT and instr rules, it is most likely that those disappeared lemmas will still be used. Neverthless, making them separated from the type language and its meta theory is important because it reduces the size of the type language, as well as allows more flexible reasoning. By introducing meta implication into TAL, we made one step forward so now there is a mixture of syntactic types and logic proofs.

We call this version of TAL a semantic TAL (STAL). STAL and TAL share the exactly same syntax and top-level static semantics, as well as the same state and value typing rules (The remaining of Figure 4). While STAL has much more reasoning power than TAL do, the soundness of STAL are simpler than TAL’s. Nevertheless, instead of merely supplying type signatures to their code, now the programmers have to also supply actual meta logic proof.

As an intermediate step from TAL toward CAP, STAL only upgrades TAL’s expressiveness by using general logic implications in the subtyping and instruction typing rules. STAL program specifications are still fullly syntactic types and thus are not as expressive as general logic predicate.

It is obvious to obtain the following TAL to STAL typing translation theorm. (we ignore the cases of those judgments where TAL and STAL share the exactly same rules.)

Theorem 2 (Typing Preservations from TAL to STAL).

1. if ⊢_{TAL} [Δ].Γ ≤ [Δ′].Γ′ then ⊢_{STAL} [Δ].Γ ≤ [Δ′].Γ′;

2. if ⊢_{TAL} {Γ}c{Γ′} then ⊢_{STAL} {Γ}c{Γ′}.

4 Target Language: XCAP+

4.1 XCAP: A Certified Assembly Programming Language

Certified assembly programming (CAP) [15] is logic-based verification framework for assembly code. Recently, XCAP [27], a language following CAP, was proposed to solve the problem of modular support of higher-order features like embedded code pointers (ECPs) and impredicative polymorphisms. This paper uses XCAP as the base language for the target of translation from TAL.

Figure 5 defines the core of the XCAP specification language called extended logical propositions (PropX). PropX can be viewed as a lifted version of the meta logic propositions, extended with an cptr constant to specify ECPs. PropX can be used to construct assertions on machine states. For example, to specify that r1, r2, and r3 store the same value, we write λ(ℍ,ℝ).⟨ℝ(r1)=ℝ(r2)∧ ℝ(r_{2})=ℝ(r3) ⟩. We also define code heap specifications and assertion subsumption (⇒) accordingly.

To establish the validity of extended propositions, XCAP defines a set of inductively defined validity rules in Figure 6. The judgment, Γ ⊢_{Ψ} P, means that P is valid under environment Γ (a set of extended propositions) and code heap specification Ψ. The introduction rules of lifted proposition ⟨p⟩and ECP proposition cptr(f,a) require that p and Ψ(f) =a be valid in the meta logic. The interpretation of extended propositions is defined as their validity under the empty environment: [[P]]_{Ψ} ≜ · ⊢_{Ψ} P.

We present the XCAP inference rules also in Figure 5. Comparing to TAL’s top-level static semantics, we can see that they share similar structures. This is convenient for the later translation. Due to space constraint, we only explain the rules that are different from TAL.

In the top level rule, the current state is checked upon the interpretation of current assertion. For simple instructions, we require the pre- and post-condition satisfy the

Ψ ⊢{a}ℙ (Well-formed Program)

\begin{matrix}⊢ ℂ:Ψ  ([[a]]_{Ψ} 𝕊)  Ψ ⊢\{a\}𝕀 \\ Ψ ⊢\{a\}(ℂ,𝕊,𝕀) \end{matrix} (prog)

⊢ ℂ:Ψ (Well-formed Code Heap)

\begin{matrix}Ψ ⊢\{Ψ(f) \}ℂ(f)  ∀f∈dom(Ψ) \\ ⊢ ℂ:Ψ \end{matrix} (cdhp)

Ψ ⊢{a}𝕀 (Well-formed Instruction Sequence)

(CdHpSpec) Ψ ::= {f⇝ a}^{∗}
(Assertion) a ∈ State → PropX
(PropX) P,Q ::= ⟨p⟩| cptr(f,a)
| P∧ ∧ Q | P∨ ∨ Q | P→ → Q
| ∀∀x:A.P | ∃∃x:A.P
| ∃∃α:A→ PropX. P
[[a]]_{Ψ} ≜ λ𝕊. [[a 𝕊]]_{Ψ}
a⇒a′ ≜ ∀Ψ,𝕊. [[a]]_{Ψ} 𝕊⊃[[a′]]_{Ψ} 𝕊
a ⇒c a′≜ ∀Ψ,𝕊. [[a]]_{Ψ} 𝕊⊃[[a′]]_{Ψ} Nextc(𝕊)
a ⇒c a′  Ψ ⊢{a′}𝕀 c∈{add,mov,movi,ld,st} Ψ ⊢{a}c;𝕀 (seq)  (λ𝕊.cptr(f,Ψ(f) )∧ ∧ a 𝕊) ⇒ a′ f∈dom(Ψ)  Ψ ⊢{a′}𝕀 Ψ ⊢{a}𝕀 (ecp)
a ⇒ Ψ(f)  f∈dom(Ψ) Ψ ⊢{a}jdf (jd)  a ⇒ (λ(ℍ,ℝ).a′(ℍ,ℝ) ∧ ∧ cptr(ℝ(r),a′)) Ψ ⊢{a}jmpr (jmp)
(λ(ℍ,ℝ).⟨ℝ(r_{s})≤i ⟩∧ ∧ a (ℍ,ℝ)) ⇒ a′  Ψ ⊢{a′}𝕀
(λ(ℍ,ℝ).⟨ℝ(r_{s})>i ⟩∧ ∧ a (ℍ,ℝ)) ⇒ Ψ(f)  f∈ dom(Ψ)

Ψ ⊢{a}bgtir_{s},i,f;𝕀

(bgti)

Fig. 5. Assertion language and inference rules for XCAP

Γ ⊢_{Ψ} P (Validity of Extended Propositions) (The following omits the Ψ in Γ ⊢_{Ψ} P.)

(env) Γ:= · | Γ,P {P ∈ Γ \atop Γ ⊢P} (env) {p \atop Γ ⊢⟨p⟩} (⟨⟩-i) {Γ ⊢⟨p⟩ p ⊃ (Γ ⊢Q) \atop Γ ⊢Q} (⟨⟩-e)
Ψ(f) =a ; Γ ⊢cptr(f,a) (cp-i) Γ ⊢cptr(f,a) (Ψ(f) =a)⊃(Γ ⊢Q) Γ ⊢Q (cp-e)  {Γ ⊢P Γ ⊢Q \atop Γ ⊢P∧ ∧ Q} (∧ ∧ -i)
{Γ ⊢P∧ ∧ Q \atop Γ ⊢P} (∧ ∧ -e1)  {Γ ⊢P∧ ∧ Q \atop Γ ⊢Q} (∧ ∧ -e2)  {Γ ⊢P \atop Γ ⊢P∨ ∨ Q} (∨ ∨ -i1)  {Γ ⊢Q \atop Γ ⊢P∨ ∨ Q} (∨ ∨ -i2)
{Γ ⊢P∨ ∨ Q Γ,P ⊢R Γ,Q ⊢R \atop Γ ⊢R} (∨ ∨ -e)  {Γ,P ⊢Q \atop Γ ⊢P→ → Q} (→ → -i)  {Γ ⊢P→ → Q Γ ⊢P \atop Γ ⊢Q} (→ → -e)
{Γ ⊢P[B/x] ∀ B:A \atop Γ ⊢∀∀x:A.P} (∀∀-i1)  {Γ ⊢∀∀x:A.P B:A \atop Γ ⊢P[B/x]} (∀∀-e1)  {B:A Γ ⊢P[B/x] \atop Γ ⊢∃∃x:A.P}(∃∃-i1)
{Γ ⊢∃∃x:A.P  Γ,P[B/x]⊢Q  ∀ B:A \atop Γ ⊢Q} (∃∃-e1)  a:A→ PropX Γ ⊢P[a/α] Γ ⊢∃∃α:A→ PropX. P (∃∃-i2)

Fig. 6. Validity rules for extended propositions (PropX)

weakest precondition relation. Direct jump is safe as long as the target code’s precondition is weaker than the current one. For indirect jump, the current precondition has to guarantee that the target address is a well-formed code label with a weaker precondition. The ecp rule allows one to introduce new ECP propositions about any labels in the code heap specification into the new assertion.

Consistency of PropX interpretation, “[[⟨False⟩]]_{Ψ} is not provable,” is merely a corollary of the following theorem.

Theorem 3 (Soundness of PropX Interpretation).

1. If [[⟨p⟩]]_{Ψ} then p;

2. if [[cptr(f,a)]]_{Ψ} then Ψ(f) = a;

3. if [[P∧ ∧ Q]]_{Ψ} then [[P]]_{Ψ} and [[Q]]_{Ψ};

4. if [[P∨ ∨ Q]]_{Ψ} then either [[P]]_{Ψ} or [[Q]]_{Ψ};

5. if [[P→ → Q]]_{Ψ} and [[P]]_{Ψ} then [[Q]]_{Ψ};

6. if [[∀∀x:A.P]]_{Ψ} and B:A then [[P[B/x]]]_{Ψ};

7. if [[∃∃x:A.P]]_{Ψ} then there exists B:A such that [[P[B/x]]]_{Ψ};

8. if [[∃∃α:A→ PropX. P]]_{Ψ} then there exists a:A→ PropX such that [[P[a/α]]]_{Ψ}.

The soundness of XCAP is also proved in the similar way as for TAL.

Theorem 4 (XCAP Soundness). If Ψ ⊢{a}ℙ , then for any natural number n, there exists a program ℙ′such that ℙ⟼→^{n} ℙ′.

In the following sections, we present two extensions to XCAP. These extensions only change the assertion language and do not alter the structure of XCAP. As a result, soundness and many other meta properties of XCAP easily hold. Our extensions, including the validity soundness and XCAP soundness theorems, have been mechanized in Coq Proof Assistant [17]. Our implementation is available at [29].

4.2 Supporting Logical Recursive Specifications

Recursive specifications are very useful in describing complex invariants. Simple recursive data structures such as link-list are already supported by XCAP. However, for the recursive types (μα.τ) found in TAL, their counterpart in logic, “recursive predicates”, can not be easily defined in XCAP. We add a piece of syntax to PropX to support recursive predicates and use syntactic methods to establish their validities.

We define the recursive predicate constructor as below.

(PropX) P,Q ::= ... | (μμ α:A→ PropX.λx:A.P B)

To understand the formation of recursive predicate, let us start from the innermost proposition P. λx:A.P is a predicate of type A → PropX. So μμα: A → PropX.λx:A.P is meant to be a recursive predicate of type A → PropX, which corresponds to recursive types found in type systems. Since the basic unit of definition is extended proposition instead of extended predicate, we apply it with a term B of type A, and make (μμ α:A→ PropX.λx:A.P B)the basic shape of recursive predicates formula. When using recursive predicates formulas, we often use its predicate form, and use the notation μμα:A → PropX.λx:A.P to represent predicate λy:A.(μμ α:A→ PropX.λx:A.P y).

To establish validity of recursive predicate formulas, we add the following rule to the validity rules in Figure 6. It is essentially a fold rule for recursive types.

B:A Γ ⊢ P[B/x][μμα:A → PropX.λx:A.P/α]

Γ ⊢ (μμ α:A→ PropX.λx:A.P B) (μ-i)

We extend PropX interpretation soundness (Theorem 3) with the following case:

If [[(μμ α:A→ PropX.λx:A.P B)]]_{Ψ} then [[P[B/x][μμα:A → PropX.λx:A.P/α]]]_{Ψ}.

4.3 Supporting Logical mutable reference

Weak update (also termed as “mutable reference” or “general references”) is a commonly used memory mutation model. Examples of weak update include ML reference cells (int ref) and managed data pointers (int gc*) in .NET common type system. In the weak update model, each memory cell’s values must satisfy a certain fixed value type. The tuple type in TAL (such as the one to be shown in next section) is also a weak update reference cell types.

Unfournately, weak update is not well-supported by CAP and other Hoare-logic-based PCC systems. The problem is due to the lack of a global data heap invariant that local assertions about heap cells can be checked upon. Existing Hoare-logic-based PCC systems either avoid supporting weak update [24, 16], limit the assertions (for reference cells) to types only [30], or resort to heavyweight techniques that require the construction of complex semantic models [26, 31]. In this section we present a weak update extension of the XCAP using the similar syntactic technique for ECPs.

We add a reference cell proposition ref(l,t) to the extended propositions. It associates word type t (a value predicate) with data label l.

(PropX) P,Q ::= ... | ref(l,t)
(WordTy )  t  ∈ Word→ PropX

We can use the following macro to describe a record of n cells.

record(l,t_{1},...,t_{n}) ≜ ref(l,t_{1})∧ ∧ ... ∧ ∧ ref(l+n−1,t_{n})

To testify the validity of reference cell propositions, in the interpretation [[P]]_{Ψ,Φ} we need an additional “data heap specification” parameter Φ which, similar to the code heap specification Ψ, is a partial mapping from data labels to word types.

(DtHpSpec) Φ ::= {l ⇝ t}^{∗}

To establish validity of ref(l,t), data label l and word type t need to be in Φ.

{Φ(l) =t \atop Γ ⊢_{Ψ,Φ} ref(l,t)} (rf-i)  Γ ⊢_{Ψ,Φ} ref(l,t) (Φ(l) =t)⊃(Γ ⊢Q) Γ ⊢_{Ψ,Φ} Q (rf-e)

Validity rules of other cases remain unchanged other than taking an extra Φ argument. Validity soundness of those cases also holds, with the following additional case.

If [[ref(l,t)]]_{Ψ,Φ} then Φ(l) = t;

Different from code heap, the data heap is dynamic. Its specification can not be obtained statically. Instead, we need to find it out in each execution steps. So the assertion interpretation is changed to:

[[a]]_{Ψ} ≜ λ(ℍ,ℝ).∃Φ,ℍ_{s},ℍ_{w}. ℍ=ℍ_{s}⊎ℍ_{w}∧ [[a (ℍ_{s},ℝ)]]_{Ψ,Φ} ∧ DH Ψ Φ ℍ_{w}

There should exist a data heap specification Φ describing the weak update part of current data heap. Other than checking validity of (a (ℍ,ℝ)) using Ψ and Φ, we also needs to checking validity of Φ.

For a data heap specification Φ to be valid, each reference cell must contains value that matches its word type.

DH Ψ Φ ℍ ≜ ∀l∈dom(Φ) =dom(ℍ). [[Φ(l) ℍ(l)]]_{Ψ,Φ}

Based on the weak update memory model defined above, we can derived many useful “macro” inference rules below. These rules can help guide the proof process by the programmer. (insens (a,r) asserts predicate is insensitive to register r, i.e., does not talk about register r. Its definition is omitted here.)

Ψ ⊢{(λ(ℍ,ℝ).a(ℍ,ℝ)∧ ∧ t ℝ(r_{d}))}𝕀 insens (a,r_{d})
Ψ ⊢{(λ(ℍ,ℝ).a(ℍ,ℝ)∧ ∧ ref(ℝ(r_{s})+w,t) )}ldr_{d},r_{s}(w);𝕀

(w-ld)

Ψ ⊢{a}𝕀
Ψ ⊢{(λ(ℍ,ℝ).a(ℍ,ℝ)∧ ∧ ref(ℝ(r_{d})+w,t) ∧ ∧ t ℝ(r_{s}))}st r_{d}(w),r_{s};𝕀

(w-st)

To avoid confusion, we call the XCAP language plus the logical recursive specification and logical mutable reference extension as the XCAP+ language, which serves as the target language of the translation.

Example Below is a “mini object”, using the recursive predicates and weak update extensions presented in previous sections.

    classs c {
      void f (c x) { x.f(x) }
    }

c ≜ μμ α:Word →PropX.λx:Word.ref(x, λy:Word.cptr(y, λ(ℍ,ℝ).(α ℝ(r1))))

The above example may looks similar to what one would normally write in a syntactic type system. However, given the ability to write general logic predicate in the sepcifications, it is possible to compose very interesting data structures and properties. Below is an example: a record pointer l which points to an even number, a data pointer to a reference cell storing an odd number, and a code pointer which, among other things, expects register r_{1} to be an unaliased pointer to a prime number. (↦ and ∗ are separation logic connectives which can be build in XCAP using shallow embedding.)

record(l, even, λw.ref(w,odd), λw.cptr(w, λ(ℍ,ℝ).(∃∃w. ℝ(r_{1})↦w ∧ prime w) ∗ ...))

Translation from TAL WordTy to XCAP+ WordTy

⌜int⌝ ≜ λw.True
⌜code [Δ].Γ⌝ ≜ λw.codeptr(w,⌜[Δ].Γ⌝)
⌜⟨τ_{1},...,τ_{n}⟩⌝ ≜ λw.record(w,⌜τ_{1}⌝,...,⌜τ_{n}⌝)
⌜∃α. τ⌝ ≜ λw.∃∃α:Word →PropX.⌜τ⌝
⌜μα.τ⌝ ≜ λw.(μμ α:Word →PropX.λx:Word.(⌜τ⌝ x) w)

Translation from TAL Precondition to XCAP+ Assertion ⌜[α_{1},...,α_{m}].{r_{1}⇝τ_{1},...,r_{n}⇝τ_{n}}⌝

≜ λ(ℍ,ℝ).∃∃α_{1},...,α_{m}: Word →PropX. (⌜τ_{1}⌝ ℝ(r_{1}))∧ ∧ ... ∧ ∧ (⌜τ_{n}⌝ ℝ(r_{n}))

Translation from TAL CdHpSpec to XCAP+ CdHpSpec

⌜{l_{1}⇝[Δ_{1}].Γ_{1},...,l_{n}⇝[Δ_{n}].Γ_{n}}⌝ ≜ {l_{1}⇝⌜[Δ_{1}].Γ_{1}⌝,...,l_{n}⇝⌜[Δ_{n}].Γ_{n}⌝}

Translation from TAL DtHpSpec to XCAP+ DtHpSpec

⌜{l_{1}⇝τ_{1},...,l_{n}⇝τ_{n}}⌝ ≜ {l_{1}⇝⌜τ_{1}⌝,...,l_{n}⇝⌜τ_{n}⌝}

Fig. 7. Type translations from TAL/STAL to XCAP+

5 A Translation from TAL/STAL to XCAP+

We first give a translation from TAL/STAL types to XCAP+ assertions. We then show the type-preserving property of the STAL to XCAP+ translation. Finally we do some brief discussion of the translation.

5.1 Type Translations from TAL/STAL to XCAP+

We present the type translations from TAL to XCAP+ in Figure 7. Various ⌜·⌝translate TAL types into XCAP+ assertions and specifications.

In the word type translation, integer type becomes a tautology as any machine word can be treated as an integer. Code type is translated into ECP formulas. Tuple types in TAL is translated into record type in XCAP+. Existential types and recursive types in TAL are also translated into their XCAP+ counterparts.

The translation of a TAL precondition, which is a type variable environment plus a register file type, is an XCAP+ assertions. The type variables in the environment are now existentially quantified over XCAP+ word types at the outmost of the target assertion. The register file typing corresponds to a bunch of conjunction of register value checking.

The translations of TAL code and data heap specifications are carried out by simply translating each element’s type in them into XCAP+ assertions or word types, and preserving the partial mapping.

5.2 Typing Preservations from TAL/STAL to XCAP+

An important property of the previous type translations is whether they preserve the typing, i.e., whether well-formed TAL/STAL entities are still well-formed in XCAP+ after the translation. As the following typing preservation lemma show, all STAL typing derivations gets preserved in XCAP+ after the translations.

Theorem 5 (Typing Preservations from STAL to XCAP+).

1. If Ψ ⊢_{STAL}{[Δ].Γ}ℙ then ⌜Ψ⌝ ⊢_{XCAP+}{⌜[Δ].Γ⌝}ℙ;

2. if ⊢_{STAL} ℂ:Ψ then ⊢_{XCAP+} ℂ:⌜Ψ⌝ ;

3. if Ψ ⊢_{STAL} {[Δ].Γ}𝕀 then ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ].Γ⌝}𝕀;

4. if Ψ ⊢_{STAL} 𝕊:[Δ].Γ then [[⌜[Δ].Γ⌝]]_{⌜Ψ⌝} 𝕊;

5. if Ψ ⊢_{STAL} ℍ:Φ then DH ⌜Ψ⌝ ⌜Φ⌝ ℍ;

6. if Ψ;Φ ⊢_{STAL} ℝ:Γ then [[⌜[].Γ⌝(ℍ,ℝ)]]_{⌜Ψ⌝ ,⌜Φ⌝};

7. if Ψ;Φ ⊢_{STAL} w:τ then [[⌜τ⌝w]]_{⌜Ψ⌝ ,⌜Φ⌝};

8. if ⊢_{STAL} [Δ].Γ ≤ [Δ′].Γ′ then ⌜[Δ].Γ⌝ ⇒ ⌜[Δ′].Γ′⌝;

9. if ⊢_{STAL} {Γ}c{Γ′} then ⌜[Δ].Γ⌝_{Ψ} ⇒c ⌜[Δ].Γ′⌝.

Proof.We show selected cases for (3). By induction over the structure of Ψ ⊢_{TAL} {[Δ].Γ}𝕀 .

case weaken. \begin{matrix}⊢ [Δ].Γ ≤ [Δ′].Γ′ & Ψ ⊢\{[Δ′].Γ′\}𝕀 \\ Ψ ⊢\{[Δ].Γ\}𝕀 \end{matrix}

By induction hypothesis it follows that ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ′].Γ′⌝}𝕀. The following weakening lemma easily holds for XCAP+: “if Ψ ⊢{a′}𝕀 and a ⇒ a′then Ψ ⊢{a}𝕀 ”. By (8) it follows that ⌜[Δ].Γ⌝ ⇒ ⌜[Δ′].Γ′⌝. Thus it follows that ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ].Γ⌝}𝕀.

case seq.  Ψ ⊢{Γ}c{Γ′}  Ψ ⊢{[Δ].Γ′}𝕀  c∈{add,mov,movi,ld,st} Ψ ⊢{[Δ].Γ}c;𝕀

By induction hypothesis it follows that ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ].Γ′⌝}𝕀. By (9) it follows that ⌜[Δ].Γ⌝_{Ψ} ⇒c ⌜[Δ].Γ′⌝. By rule seq it follows that ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ].Γ⌝}c;𝕀.

case jd.  f∈dom(Ψ)  ⊢ [Δ].Γ ≤ Ψ(f) Ψ ⊢{[Δ].Γ}jdf

By (8) it follows that ⌜[Δ].Γ⌝ ⇒ ⌜Ψ(f) ⌝, and then ⌜[Δ].Γ⌝ ⇒ ⌜Ψ⌝ (f). By rule jd it follows that ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ].Γ⌝}jdf.

case jmp.  Γ(r) =code [Δ′].Γ′ ⊢ [Δ].Γ ≤ [Δ′].Γ′ Ψ ⊢{[Δ].Γ}jmpr

By translation it follows that ⌜[Δ].Γ⌝⇒ λ(ℍ,ℝ).cptr(ℝ(r),⌜[Δ′].Γ′⌝). By (8) it follows that ⌜[Δ].Γ⌝ ⇒ ⌜[Δ′].Γ′⌝. By rule jmp it follows that ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ].Γ⌝}jmpr.

case movf.  f∈dom(Ψ)  Ψ ⊢{[Δ].Γ{r_{d}⇝code Ψ(f) }}𝕀 Ψ ⊢{[Δ].Γ}movi r_{d},f;𝕀

By induction hypothesis it follows that ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ].Γ{r_{d}⇝code Ψ(f) }⌝}𝕀. By rule ECP and SEQ it follows that ⌜Ψ⌝ ⊢_{XCAP+} {⌜[Δ].Γ⌝}movi r_{d},f;𝕀. ■

5.3 Discussion

We discussed the relationship between TAL and CAP by showing a translation from TAL to XCAP+. However, this work is by no means limited to the translation itself.

For example, one can treat the translation as a shallow embeddeding of TAL types and typing rules in XCAP+, which means there is no need to build meta theory for TAL while still letting the programmer working at TAL level.

One interesting perspective to view the XCAP+ system is from TAL programmer’s side. When writting programs that will interact with XCAP+ code that involve complex logical specification not expressible in TAL, so long as the interfaces abstract and hide that part of “real” logical specification (e.g., by using existential packages), and local code behavior is simple enough (which is usually the case), the programmers can “pretend” that they are dealing with external TAL code instead of XCAP+ ones, by using the macros and lemmas defined for the translations. This lowers the requirement on programmers, as they do not need to learn XCAP+, even if they are dealing with external XCAP+ code.

6 Related Work and Conclusion

Hamid and Shao [30] introduced an Extensible TAL with Runtime System (XTAL) and showed its translation to an earlier version of Certified Assembly Programming. Their main goal is to make sure the translation result can interoperate with the run-time system written and verified in CAP and thus form a complete FPCC proof. Since CAP does not have modular support of embedded code pointer and weak update, the translation there can not be merely from XTAL value types to CAP predicates, but rather needs XTAL heap types as well. This requires both the source type systems and programs to be fixed.

Chen et al [4] have developed LTAL, a low-level typed assembly language which is used to compile core ML to FPCC. LTAL is based in turn upon an abstraction layer, TML (typed machine language) [32], which is an even lower-level intermediate language. Complex parts of the semantic proofs, such as the indexed model of recursive types and stratified model of mutable fields, are hidden in the soundness proof of TML.

Recently, Appel et al [33] proposed a new modal model for expressing recursive and impredicatively quantified types with mutable reference. Their method uses a Kripke semantics of the Godel-Lob logic of provability. To support mutable reference, they include the memory mapping information in the “world”. A full comparison between the CAP/XCAP line of work and the line of index-based semantic FPCC work will be an interesting yet non-trivial problem. Here we are only going to list a few of them.

First, CAP is designed to support more than ”type safety” at each program point. The code heap specification specifies the safety policy in general logic predicates, and is completely customizable. Meta theory of CAP guarantees that these safety policy is actually observable. While in indexed FPCC work, the definition of “codeptr” has always been based on a non-stuckness safety. It remains unclear how to change the definition of “codeptr” in order to support customizable and observable safety policies without rebuilding the meta theory.

Second, CAP is designed to support directly verifying assembly programs with non-trivial properties not expressible in traditional types. Various examples of CAP programs has been mechanically certified [22, 16, 18, 27]. While the indexed FPCC work has been focusing on type-preserving compilations from high-level languages, thus have few application of direct verification at assembly level. The translation presented in this paper is one effort on connecting CAP/XCAP with high-level languages.

Conclusion We presented a type-preserving translation from a TAL language to a CAP language. Our translation supports polymorphic code, mutable reference, existential, and recursive types. To do so, we used an intermediate “semantic” TAL language. We also extended the XCAP language to support logical recursive specifications and mutable references. Our result will lead to linking and inter-operating well-typed programs from traditional certifying compilers with certified libraries by CAP-like systems.

References

1. Necula, G.: Proof-carrying code. In: Proc. 24th ACM Symposium on Principles of Programming Languages, New York, ACM Press (1997) 106–119

2. Colby, C., Lee, P., Necula, G., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: Proc. 2000 ACM Conference on Programming Language Design and Implementation, New York, ACM Press (2000) 95–107

3. Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. In: Proc. 17th Annual IEEE Symposium on Logic in Computer Science. (2002) 89–100

4. Chen, J., Wu, D., Appel, A.W., Fang, H.: A provably sound tal for back-end optimization. In: Proc. 2003 ACM Conference on Programming Language Design and Implementation, ACM Press (2003) 208–219

5. Crary, K.: Toward a foundational typed assembly language. In: Proc. 30th ACM Symposium on Principles of Programming Languages. (2003) 198

6. Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley (1996)

7. Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge, Massachusetts (1997)

8. Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. In: Proc. 25th ACM Symposium on Principles of Programming Languages, ACM Press (1998) 85–97

9. Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proc. 26th ACM Symposium on Principles of Programming Languages, ACM Press (1999) 214–227

10. Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: A type system for certified binaries. In: Proc. 29th ACM Symposium on Principles of Programming Languages, ACM Press (2002) 217–232

11. Crary, K., Vanderwaart, J.C.: An expressive, scalable type theory for certified code. In: Proc. 7th ACM SIGPLAN International Conference on Functional Programming. (2002) 191–205

12. Ahmed, A., Walker, D.: The logical approach to stack typing. In: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, ACM Press (2003) 74–85

13. Ahmed, A., Jia, L., Walker, D.: Reasoning about hierarchical storage. In: Proc. 18th IEEE Symposium on Logic in Computer Science. (2003) 33–44 14. Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proc. 17th

Annual IEEE Symposium on Logic in Computer Science. (2002)

15. Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming 50(1-3) (2004) 101–127

16. Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: Proc. 2004 International Conference on Functional Programming (ICFP’04). (2004)

17. The Coq Development Team: The Coq proof assistant reference manual. The Coq release v8.0 (2004)

18. Feng, X., Shao, Z.: Modular verification of concurrent assembly code with dynamic thread creation and termination. In: Proc. 2005 International Conference on Functional Programming (ICFP’04). (2005)

19. Floyd, R.W.: Assigning meaning to programs. Communications of the ACM (1967)

20. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM (1969)

21. Appel, A.W.: Foundational proof-carrying code. In: Proc. 16th Annual IEEE Symposium on Logic in Computer Science. (2001) 247–258

22. Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: Dynamic storage allocation. In: Proc. 2003 European Symposium on Programming (ESOP’03). (2003)

23. Gordon, M.: A mechanized Hoare logic of state transitions. In Roscoe, A.W., ed.: A Classical Mind—Essays in Honour of C.A.R. Hoare, Prentice Hall (1994) 143–160

24. Necula, G.: Compiling with Proofs. PhD thesis, School of Computer Science, Carnegie Mellon Univ. (1998)

25. Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proofcarrying code. In: Proc. 27th ACM Symposium on Principles of Programming Languages. (2000) 243–253

26. Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proofcarrying code. ACM Transactions on Programming Languages and Systems 23(5) (2001) 657–683

27. Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: Proc. 33rd ACM Symposium on Principles of Programming Languages. (2006)

28. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1) (1994) 38–94

29. Ni, Z., Shao, Z.: Implementation for a translation from typed assembly language to certified

assembly programming. http://flint.cs.yale.edu/publications/talcap.html

(2006)

30. Hamid, N.A., Shao, Z.: Interfacing hoare logic and type systems for foundational proofcarrying code. In: Proc. 17th International Conference on Theorem Proving in Higher Order Logics. Volume 3223 of LNCS., Springer-Verlag (2004) 118–135

31. Ahmed, A.J.: Semantics of Types for Mutable State. PhD thesis, Princeton University (2004)

32. Swadi, K.N., Appel, A.W.: Typed machine language and its semantics. Unpublished

manuscript available at www.cs.princeton.edu/~appel/papers (2001)

33. Appel, A.W., Mellies, P.A., Richards, C.D., Vouillon., J.: A very modal model of a modern, major, general type system. In: Proc. 34th ACM Symposium on Principles of Programming Languages. (2007)