Link 2.Basic settings CTL threaded proof program In order to certify CTL in the FPCC framework.we linked SCAP program CMAP formalize all the related concepts into a mechanized meta- logic.In other words,the machine model,the code of CTL OCAP its specifications,program logics and related safety proof Cic(Coq) are all based on a common formal logic,resulting in smaller trusted computing base for safety.In this section,we will Figure 1.The OCAP framework present these basic settings. tween CTL and multithreaded programs due to the absence The mechanized meta-Logic.We use the calculus of in- of safety proof for the code with respect to linkage.Al- ductive constructions (CiC)[21]as our meta-logic.CiC is though the construction of such safety proof is possible,it supported by the Cog proof assistant [3],which we use to is non-trivial because of the differences between specifica- implement the work presented in this paper. tion languages,as well as certification methods'variety. Recently,Feng et al.[6]proposed an open certification The target machine.A MIPS-style [15]target machine framework(OCAP)to support inter-operation of different (TM)is chosen as our machine model on which our thread certification systems.OCAP serves as a common layer in library runs.We omit some physical machine features which different program logics can be embedded. irrelevant to threading,such as address alignment,bits- Based on OCAP,we demonstrate in this paper the link- arithmetic etc..The target machine and its operational se- age between CTL certified in SCAP and user programs cer- mantics are formally defined in Figure 2.A machine pro- tified in CMAP.and construct the extra safety proof of in- gram P contains a code heap C and an updatable state S.A teraction,as shown in Figure 1. code heap C is a segment of memory mapping addresses to The main contributions of our work are as follows: machine instructions,but C is read-only and isolated from the mutable data heap H.The state S,which specifies the We describe,specify,and certify a simple but real- execution of the program,consists of a register file,muta- istic thread library CTL.It provides common multi- ble data heap H and the program counter pc.The target threading features including thread scheduling,dy- machine has 32 general-purpose registers.Following the namic thread creation,termination and joining. MIPS convention,the table below shows the register alias We define formal specifications to capture the seman- and usage. tics of CTL routines.This library carries machine- checkable proof which ensures that the library does not r0 IO always zero vo-v1 r2-r3 return values a0-a3 r4-r7 arguments to-t7 rs-ris temporary violate the safety policies. k0-k1 r26-r27 reserved ra r31 return address Meanwhile,we adapt and embed CMAP in a simpli- The basic TM instruction set covers the common MIPS fied OCAP framework.Thus.CTL can be linked to instructions for arithmetics,jump,conditional branch and the user programs certified in CMAP to construct an load/store.It is easy to add more instructions in our TM. integrated mechanized FPCC package.As far as we The relation PP indicates that the program state P know,CTL is the first thread library which can be steps to the program state P.The relation PP means safely linked to multithreaded user programs. that P reaches P in k steps,and*is the reflexive and We have formalized the work presented in this paper, transitive closure of the step relation.The auxiliary func- including CTL,OCAP.CMAP,and their soundness proof, tion Next(-)specifies the state transition according to the in the Coq proof assistant [3].Interested readers may find operational semantics instruction t.We use the notation S them on our web site [11]. to denote Next(S). The remainder of this paper is organized as follows:Sec- tion 2 presents the formalization of basic settings.In Sec- Safety.Safety of the program means that:(i)the execution tion 3 we describe and certify the CTL library.We dis- of the programs in CTL will not go stuck;(ii)the code of cuss the verification framework CMAP in which the mul- CTL satisfies certain safety specifications.The code heap tithreaded programs are certified in Section 4.Section 5 specification y is a map from code labels f to code specifi- shows the linkage of CTL and user programs in a simpli- cations 0,as defined below: fied OCAP framework.Section 6 is related work and the (CdSpec）6=… conclusion. (CHSpec）Ψ：={fo}￾
              
 



  ￾        
                   Figure 1. The OCAP framework tween CTL and multithreaded programs due to the absence of safety proof for the code with respect to linkage. Al￾though the construction of such safety proof is possible, it is non-trivial because of the differences between specifica￾tion languages, as well as certification methods’ variety. Recently, Feng et al. [6] proposed an open certification framework (OCAP) to support inter-operation of different certification systems. OCAP serves as a common layer in which different program logics can be embedded. Based on OCAP, we demonstrate in this paper the link￾age between CTL certified in SCAP and user programs cer￾tified in CMAP, and construct the extra safety proof of in￾teraction, as shown in Figure 1. The main contributions of our work are as follows: • We describe, specify, and certify a simple but real￾istic thread library CTL. It provides common multi￾threading features including thread scheduling, dy￾namic thread creation, termination and joining. • We define formal specifications to capture the seman￾tics of CTL routines. This library carries machine￾checkable proof which ensures that the library does not violate the safety policies. • Meanwhile, we adapt and embed CMAP in a simpli- fied OCAP framework. Thus, CTL can be linked to the user programs certified in CMAP to construct an integrated mechanized FPCC package. As far as we know, CTL is the first thread library which can be safely linked to multithreaded user programs. We have formalized the work presented in this paper, including CTL, OCAP, CMAP, and their soundness proof, in the Coq proof assistant [3]. Interested readers may find them on our web site [11]. The remainder of this paper is organized as follows: Sec￾tion 2 presents the formalization of basic settings. In Sec￾tion 3 we describe and certify the CTL library. We dis￾cuss the verification framework CMAP in which the mul￾tithreaded programs are certified in Section 4. Section 5 shows the linkage of CTL and user programs in a simpli- fied OCAP framework. Section 6 is related work and the conclusion. 2. Basic settings In order to certify CTL in the FPCC framework, we formalize all the related concepts into a mechanized meta￾logic. In other words, the machine model, the code of CTL, its specifications, program logics and related safety proof are all based on a common formal logic, resulting in smaller trusted computing base for safety. In this section, we will present these basic settings. The mechanized meta-Logic. We use the calculus of in￾ductive constructions (CiC) [21] as our meta-logic. CiC is supported by the Coq proof assistant [3], which we use to implement the work presented in this paper. The target machine. A MIPS-style [15] target machine (TM) is chosen as our machine model on which our thread library runs. We omit some physical machine features irrelevant to threading, such as address alignment, bits￾arithmetic etc.. The target machine and its operational se￾mantics are formally defined in Figure 2. A machine pro￾gram P contains a code heap C and an updatable state S. A code heap C is a segment of memory mapping addresses to machine instructions, but C is read-only and isolated from the mutable data heap H. The state S, which specifies the execution of the program, consists of a register file, muta￾ble data heap H and the program counter pc. The target machine has 32 general-purpose registers. Following the MIPS convention, the table below shows the register alias and usage. r0 r0 always zero v0−v1 r2 −r3 return values a0−a3 r4 −r7 arguments t0−t7 r8 −r15 temporary k0−k1 r26 −r27 reserved ra r31 return address The basic TM instruction set covers the common MIPS instructions for arithmetics, jump, conditional branch and load/store. It is easy to add more instructions in our TM. The relation P 7−→ P ′ indicates that the program state P steps to the program state P ′ . The relation P 7−→k P ′ means that P reaches P ′ in k steps, and 7−→∗ is the reflexive and transitive closure of the step relation. The auxiliary func￾tion Nextι( ) specifies the state transition according to the operational semantics instruction ι. We use the notation Sˆ ι to denote Nextι(S). Safety. Safety of the program means that:(i) the execution of the programs in CTL will not go stuck; (ii) the code of CTL satisfies certain safety specifications. The code heap specification Ψ is a map from code labels f to code specifi- cations θ, as defined below: (CdSpec) θ ::= ··· (CHSpec) Ψ ::= {f ❀ θ} ∗