1% 2% Copyright 2014, NICTA 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(NICTA_GPL) 9% 10 11\chapter{Introduction} 12 13This document provides formal proofs in the interactive theorem prover 14Isabelle/HOL~\cite{Nipkow_PW:Isabelle} of certain correctness properties of 15generated communication code of the \camkes platform~\cite{Kuz_LGH_07}. 16These proofs are example output of a generalised proof generation tool and 17are intended to extend previous reports that describe the 18static~\cite{Fernandez_KKM_13:tr} and dynamic~\cite{Fernandez_GAKK_13:tr} 19semantics of \camkes systems. 20The previous formalisms gave a high-level specification of the behaviour of 21\camkes systems, while the current proofs reason about the behaviour of the 22glue code at the level of C, targeting the seL4 23microkernel~\cite{Klein_EHACDEEKNSTW_09}. 24 25The proofs that follow are constructed on an abstraction of C code. 26This abstraction process is performed by two existing 27tools, a translation from C to the generic imperative language 28SIMPL~\cite{Winwood_KSACN_09}, and a further abstraction by the tool 29AutoCorres~\cite{Greenaway_LAK_14}, neither of which are specific 30to \camkes. 31These tools lift a C translation unit into monadic specifications of the 32contained functions. 33Alongside the generated code, we automate the production of proofs of 34correctness properties of these specifications. 35These proofs leverage an Isabelle 36tactic that performs weakest pre-condition reasoning. 37 38\camkes has three different communication modes: synchronous, asynchronous and 39shared memory. 40These are implemented as three \camkes primitives, remote procedure calls 41(RPCs), events and dataports, respectively. 42The desirable correctness property of connector glue code is dependent on which 43of these the connector implements. 44For example, remote procedure call connectors should ensure, among other 45things, that the function call and parameters that are sent by the caller are 46correctly received and decoded by the callee. 47A common requirement for all the glue code is safe execution with respect to 48the C standard and the state of the system at runtime. 49The generated proofs given in the following chapters show this for three 50specific connectors, one for each \camkes communication primitive, but the 51proof generation process generalises to other \camkes connectors as well. 52This property requires that the glue code only accesses valid memory, that it 53obeys the restrictions of the C99 standard~\cite{C99} and that it always 54terminates. 55 56In proving this behaviour of the glue code, we rely on some explicit 57assumptions on user code within the system. 58In particular, we assume that the user code also obeys the C99 standard and 59does not modify any glue code state. 60The glue code state covers memory regions relevant for communication with seL4, 61thread identification and thread-local storage. 62This state is disjoint from the expected user state; that is, non-malicious 63user code should never have cause to modify any of the glue code state. 64As for the seL4 proofs, the generated proofs of CAmkES glue code are intended 65to apply to an ARM, unicore platform and may not hold in other operating 66environments. 67 68The connectors on which the generated proofs below are based have some 69limitations that we make explicit here. 70The event connector used does not support callbacks -- 71events can only be waited on or polled for. 72The RPC connector used does not support array parameters, strings or 73user-defined data types (e.g. C structs). 74These are limitations that will be lifted in future. 75