H Aziza

B Hajri

M Mansour
email: mmansour@aub.edu.lb

A Chehab
email: chehab@aub.edu.lb

A Perez

A Lightweight Write-Assist Scheme for Reduced RRAM Variability and Power

Common problems with Oxide-based Resistive RAM are related to high variability in operating conditions and high programming currents during FORMING, SET and RESET operations. Although research has taken steps to resolve these issues, variability combined with high programming currents remains an important characteristic for RRAMs. In a conventional write scheme with fixed duration and amplitude, the programming current is not controlled, which degrades the cell performance (power consumption and variability) due to over-programming. In this paper, a self-adaptive write driver is proposed to control the write current. A feedback mechanism based on current comparison is used to switch off the write stimulus as soon as the preferred write current is reached. Compared to conventional write schemes, in the proposed write-assist circuit, the write energy per bit is reduced by 27% and the standard deviation of post-FORMING distributions is reduced by 57%.

Introduction

Emerging technologies such as Resistive RAMs (RRAMs) are attracting considerable attention due to their tempting characteristics such as high scalability, CMOS compatibility and non-volatility to replace current conventional memories [START_REF] Vatajelu | Nonvolatile memories: Present and future challenges[END_REF] [START_REF] Zhao | Design and analysis of crossbar architecture based on complementary resistive switching non-volatile memory cells[END_REF]. A typical RRAM device consists of two metallic electrodes that sandwich a thin dielectric layer serving as a permanent storage medium. A single RRAM bit-cell can be switched between two distinct states: High Resistance State (HRS) and Low Resistance State (LRS), representing the low ('0') and high ('1') states, respectively. The transition from HRS to LRS is referred to as SET, while the opposite transition from LRS to HRS is referred to as RESET (RST). Prior to performing SET or RST, a FORMING (FMG) step is required, which is achieved one time in the device life. The FMG step is a voltage-induced resistance switching from an initial virgin state with a very high resistance to a conductive state. High voltage is typically needed during FMG since it generates the prerequisite number of defect species within the thin dielectric layer to construct a Conductive Filament (CF) [START_REF] Nminibapiel | The Efficacy of Programming Energy Controlled Switching in Resistive Random Access Memory (R5M)[END_REF]. However, FMG increases power consumption and the high voltage can initiate thermal damage, if not controlled [START_REF] Buh | Time-dependent electroforming in NiO resistive switching devices[END_REF]. V fmg , V rst and V set are the voltages required across the RRAM cell for its operation. In the rest of the paper, a FMG, SET or RST operations will be considered as a write operation. The read-out operation is performed with a low voltage, V read , whose value is chosen to preserve the resistance state.

The conventional write scheme uses single pulse voltage with a fixed-pulse duration, resulting in over-SET and over-RST for fast RRAM cells. Consequently, power consumption is very high for such cells, especially after the resistance has been switched from HRS to LRS. Write current control remains one of the main factors for improving key performance markers of RRAMs. Indeed, it has been demonstrated that high endurance and retention are closely linked to the programming currents since excessive and insufficient currents result in failure [5] [6]. In this context, programming algorithms and write assist circuits play a crucial role on performance and yield optimization [START_REF] Wang | Improving resistance uniformity and endurance of resistive switching memory by accurately controlling the stress time of pulse program operation[END_REF]. Programverify algorithms have been developed to ensure distinct resistance distributions; they adjust the write signal (pulse number, width or amplitude) until the cell resistance reaches the target resistance state. However, in this scheme, the writing is interrupted periodically to allow for the read operations to verify that switching has occurred, which increases the write-time significantly. An alternative to avoid the use of read operations is to implement a write-termination scheme at the memory driver level where the write current pulse is cut-off right after the resistance transition completes. This prevents wasted write energy but introduces an important area overhead. For instance, in [START_REF] Yang | A self-adaptive write driver with fast termination of set-up pulse for ReRAM[END_REF], such a scheme is implemented using an op-amp, a differentiator and additional capacitors and resistors.

In this paper, we propose a cost-efficient selfterminated write driver based on write current control. Instead of detecting the resistance state transition, the driver compares the memory cell current with a reference current during write operations and terminates the write operation when the RRAM cell current matches the reference current, which is chosen high enough to ensure that write operation is complete. In addition, the reference current can be adjusted to allow a full control of the write energy. No read operation is involved in the process and no RRAM reference cells are needed. Moreover, the selfterminated write driver area overhead is very low compared to state-of-the-art write drivers. To the authors' knowledge, this is the first work which presents the integration of a compact self-adaptive write driver with a minimal area overhead (i.e. a dozen of transistors). Section 2 presents the Write-Assist Scheme. In section 3, simulation results are provided. Section 4 concludes the paper. Before its integration at a memory array level, the current comparator ability to detect a specific current is evaluated. For a set of I ref current values in the range [60µA-160µA], the cell current detection accuracy is evaluated by monitoring the comparator output. In Fig. 2, the relative current difference, ∆I, is plotted versus I ref when out_comp switches from low to high. If I ref current nominal value is considered (i.e. 100 µA), the detection precision is less than 0.1 %. For I ref variation in the range [60µA-160µA] with a 10uA step, the detection precision is in the range [-1.46%-0.94%] which demonstrates the ability of the comparator to accurately detect specific I cell values.

Proposed Scheme 2.1. Current Sensor

Vdd

Iref Icell

Vdd Vdd Either DC or pulse stress can be used to carry out a write operation. In a practical memory application, pulse programming is preferred, while DC operations are ideal for studying the switching mechanism. Thus, a pulse generator is used to operate memory cells. The memory array presented in Fig. 3 comes together with the proposed write driver presented in Fig. 4. For clarity, the write driver is associated with a single memory cell. Before any write operation, the bit line driver is enabled by setting the RS latch. If the memory cell is selected and a write '1' operation is performed (i.e. ADR and DATA signals set High), voltage pulses coming from the pulse generator, "Pulse Gen", are applied without any interruption and the cell current is measured while the write pulse is being applied. The current comparator detects whether the cell current I cell reaches the reference current I ref and turns off the pulse generator. At this point, out_comp signal goes High and resets the RS latch, which in turn disables the bit line driver (via Q signal) and turns off the pulse generator (via 𝑄 signal). At the same time, the write driver is disconnected. The next write operation starts when the RS latch is set. This scheme allows a strict control of the write current, which is highly desirable. Indeed, the transition from the HRS to the LRS during a FMG/SET operation requires current compliance to prevent destruction. As current flows, the cell resistance is reduced, and as such, more current flows as write pulses are applied. This positive feedback mechanism causes large currents to flow, which can cause permanently open or shorted cells. Therefore, current compliance in the FMG/SET direction is a requirement at the circuit level. During a RST operation, as the current flows, the resistance of the cell increases, causing current to reduce. Therefore, the RST operation is a negative feedback mechanism and a current compliance during a RST operation is not mandatory. However, having compliance in the RST direction allows an upper limit to be placed on the amount of current delivered to the cell, which is useful for power monitoring or when sizing an access device for a 1T1R architecture. The presented write scheme can be easily applied during a RST operation; the write operation is performed by biasing the memory cell in the opposite polarity. RST pulses are applied to the memory cell bottom electrode via the select transistor through the source line driver and the other terminal of the cell is connected to the current comparator.

Simulation Results and Discussion

Transient Simulation Results

We implemented the circuit in Fig. 4 using a 0.13µm High Voltage CMOS technology with a 3.5V supply voltage. As already mentioned, high voltages are needed during the FMG step, which is the first and most critical operation as it involves high currents and determines the switching characteristics during the future operation of memory cell. To verify the operation of the write scheme, SPICE simulations are performed using the Eldo simulator. Fig. 5 shows transient simulation results. Write pulses Pulse_clk (Fig. 5a) are generated without any interruption and the cell current I cell is measured and compared to the reference current I ref (Fig. 5b). As the number of pulses increases, the cell resistance decreases which in turn increases the cell current. When the cell current reaches the reference current value set to 100µA (Fig. 5b), out_comp signal switches from a low to a high level (Fig. 5c). The out_comp signal resets the RS flip-flop (Fig. 5d). As a result, RS flip-flop output Q goes low (𝑄 goes high) finishing the pulse write operation (Fig.

Monte Carlo Simulations Results

In HfO 2 -based RRAM, considered in this study, variability remains a concern since it is intrinsic to the nature of the resistive switching process [11] [12].

The exact location and size of the CF (Conductive Filament) formation and rupture cannot be reproduced from cycle to cycle or from device to device. To assess the impact of the write scheme on variability, a Monte Carlo (MC) analysis is conducted. As a result, the CF distribution size obtained from the OxRAM model is extracted. The CF size parameter is considered as a key parameter as the CF construction/destruction sets all the other parameters of the memory cell (resistance, current, etc.) [START_REF] Hamdioui | Memristor based memories: Technology, design and test[END_REF]. on post-FMG distributions after 500 MC simulation runs, using a box-plot. Several observations can be made. The median value of the CF is more important for the conventional scheme compared to the write assist scheme. This is explained by the voltage headroom reduction seen across the cell in the write assist scheme configuration. Indeed, the voltage drop across the current comparator reduces the write efficiency. Therefore, the CF size is more important in the conventional write configuration (i.e. larger conductivity). Regarding the distribution spreads, the write assist configuration clearly tightens the CF distribution spread (by 57%) and demonstrates the capability of the write assist scheme to reduce variability. Regarding the power consumption, the maximum current observed after 500 MC runs is 221µA for the conventional configuration and 100µA for the write assist configuration. The average power consumption during the entire write operation is 15.1µA for the conventional configuration and 11µA for the write assist. Simulation results are summarized in Table I.

Conclusion

The current work provides a simple and feasible solution to two of the most challenging issues in filamentary-based RRAM devices related to the control of the consumption current and the stochastic nature of the resistive switching mechanism during write operations. The presented write scheme can be used as a powerful tool for process variability and current consumption reduction during RRAM circuit operation. The write circuit is exclusively based on current control during write operations to ensure that write operations are complete for a targeted write current. The write energy per bit is reduced by 27% and the standard deviation of post-FMG distributions is reduced by 57%.

Fig. 1

 1 Fig.1shows the circuit diagram of the built-in current sensor incorporated in the write driver design. The current sensor is inserted in series between the memory cell and GND to sense the memory cell current, I cell . The sensor is in fact a current comparator inspired from Built-In Current Sensor (BICS),

Fig. 1 .

 1 Fig. 1. Built-in current comparator

Fig. 2 .

 2 Fig. 2. Current comparator evaluation2.2. Write Assist CircuitFig.3presents a part of the RRAM memory array, considered in this work, which is composed of a word line driver to select the active row (WLx), a bit line driver to select active bit (BLx) during a SET operation and a source line driver to select a specific source line (SLx) to reset a whole memory word. Sense amplifiers are used to convert the cell current into a logical value at the circuit output during a read operation. The 1T/1R memory cell (one MOS transistor in series with one resistor) is considered. Memory cells are usually grouped into 8, 16 or 32 bits to form a memory word. The memory cell is modelled by an Oxide-based RRAM model fully calibrated on silicon for a TiN/Ti/HfO 2 /TiN RRAM stack[START_REF] Bocquet | Robust compact model for bipolar oxidebased resistive switching memories[END_REF]. Either DC or pulse stress can be used to carry out a write operation. In a practical memory application, pulse programming is preferred, while DC operations are ideal for studying the switching mechanism. Thus, a pulse generator is used to operate memory cells. The memory array presented in Fig.3comes together with the proposed write driver presented in Fig.4. For clarity, the write driver is associated with a single memory cell. Before any write operation, the bit line driver is enabled by setting the RS latch. If the memory cell is selected and a write '1' operation is performed (i.e. ADR and DATA signals set High), voltage pulses coming from the pulse generator, "Pulse Gen", are applied without any interruption and the cell current is measured while the write pulse is being applied. The current comparator detects whether the cell current I cell reaches the reference current I ref and turns off the pulse generator. At this point, out_comp signal goes High and resets the RS latch, which in turn disables the bit line driver (via Q signal) and turns off the pulse generator (via 𝑄 signal). At the same time, the write driver is disconnected. The next write operation starts when the RS latch is set.

Fig. 3 .

 3 Fig. 3. Elementary memory array used for simulations

Fig. 4 .

 4 Fig. 4. Write assist circuit FMG/SET operation

Fig. 5 .

 5 Fig. 5. Transient simulation results

Fig. 6 .

 6 Fig. 6. Transient simulationTwo configurations are considered. The first one takes advantage of the write assist circuit during the write operation. The second one uses a conventional program scheme with a fixed number of programming pulses which is set to 10. This number is extracted from Fig.5e, which corresponds to the number of pulses needed to get a 100µA write current for a nominal memory cell. Since cell variability is generated based on a targeted technology (i.e. model calibrated and featuring a variability dependency) only actual possible variations are reported[START_REF] Bocquet | Robust compact model for bipolar oxidebased resistive switching memories[END_REF]. Fig.6presents the impact of the memory cell variability

TABLE I .

 I SIMULATION RESULTS

		Conv. scheme	Proposed scheme	∆(%)
	MC runs number	500	500
	Minimum CF size	0.348	0.331
	Maximum CF size	2.986	1.636
	Mean CF size	2.129	1.130
	Max. current (µA)	221	100	54.7%
	Std. deviation	0.715	0.306	57%
	Avg. current µA)	15.1	11.0	27.1%


Christopher Brown

Adam D Barwell

Yoann Marquer
email: yoann.marquer@inria.fr

Céline Minh
email: celine.minh@inria.fr

Olivier Zendra
email: olivier.zendra@inria.fr

Type-Driven Verification of Non-functional Properties

Keywords: Software and its engineering → Formal software verification, Imperative languages, Software maintenance tools, • Security and privacy → Software security engineering IDRIS, C, time, energy, security, non-functional properties, proofs, verification, contracts -> Type NatOrList False = Nat NatOrList Bool) -> NatOrList b ZeroOrNil False = Z ZeroOrNil True = []

Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification framework, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.

INTRODUCTION

Non-functional properties, such as time, energy and security, are becoming critically important in areas ranging from small-scale sensors, through smart cyber-physical systems and mobile devices, to data centres, despite it being treated as a secondary concern. As embedded devices become more commonplace, increasing is the PPDP 2019, Porto, Portugal pressing demand for more time and energy optimisation in applications that execute on them, leading to longer battery lives and more efficient software. Moreover, systems are becoming increasingly vulnerable to timing and power leakage resulting in security problems, such as side-channel attacks, for example. However, dealing with time, energy and security properties at the language level is usually a black art, where developers require the use of specialised skills, low-level tools and techniques.

Therefore, there is a clear and pressing need to expose nonfunctional concerns to the systems designer and implementor in an accessible way. What we need is a way to turn energy consumption, execution time, security level and other important (nonfunctional) program properties into first-class citizens. This will allow (non-expert) programmers to understand and directly manipulate them. Consequently, this will eliminate both the complex, time-consuming and error-prone use of extrinsic tools as well as large-scale continuous testing for non-functional program behaviour from the software engineering process and, thus, make the latter significantly more lean, agile and productive. By exposing energy, time, security, etc., as first-class citizens and by making them easy to use and understand for application programmers, we will eliminate the need for dual-expertise: the application programmer will be able to manipulate and precisely reason about energy, time, security, etc. as normal program values, directly interacting with analytical and optimisation frameworks. They will ensure that solutions meet system requirements as needed while at the same time they are highly optimised for metrics without strict requirements.

In this paper we present a novel framework, called Drive, to allow the programmer to model non-functional properties of time, energy and security in their C source-code as first-class citizens; express resource contracts on time, energy and security usage, directly through source-level constructs; and verify these contracts fully automatically using the dependently typed programming language, Idris. We give explicit proofs of these correct properties, together with a denotational semantics of our contract system. In this way, we show our system constructs verified contracts. We illustrate the technique by considering a number of examples in C, as might be commonly found in real-time embedded systems, from the Beebs benchmarks suite.

Here, ZeroOrNil is a function that takes as argument a boolean value, b. If b is False, ZeroOrNat returns Z, representing the zeroth element of the natural numbers in standard peano arithmetic, and the empty list, [], otherwise. The return type of this function therefore depends on the value of its argument. If the argument is True the return type is a natural number; if it is False, it is a list type.

Allowing types to depend upon values results in more expressive types that can be sufficiently tightly constrained in order to express some property of one or more values; e.g. that a given list is ordered. In conjunction with the Curry-Howard correspondence, where a type represents a proposition whose inhabitants represent the proof of the proposition [START_REF] Slama | Automatic generation of proof terms in dependently typed programming languages[END_REF], logical and arithmetic formulae may be expressed and reasoned about as types in a manner that is consistent with some underlying constructive logic. This allows us, for a given context, to determine not only whether some logical expression holds, but also the reason (proof) why the expression holds. Moreover, for some expressions, it is possible to automatically determine such proofs, which we discuss further in Section 5.

Deriving Models

As Drive is a fully automated framework from C source code through to a type-verified contract produced by Idris, we require a mechanism to transform C source code into Idris data-types, representing our C space of properties and assertions. In order to parse C, we make use of, and extend, an already existing C99 parser that is implemented in Haskell, called Language C 1 , which is a Haskell library providing static analyses and generation of C code. It features a complete C parser and pretty printer for the full C99 standard, and a large set of C11 CLang/GNU extensions. For this paper, we have modified and extended Language-C, so that it parses CSL statements and assertions, generating Idris code as a result. This generated Idris is then used by the Idris contract system, an example of the generated output is given in Listing 2. This allows us to fully automate our Drive framework: providing an automatic compiler from (C99) CSL to an Idris contract.

Non-functional Properties

In this paper we consider three non-functional properties that we consider to be most commonplace: energy, time and security. In terms of time, we consider the worst-case execution time (WCET ) obtained by executing the code with various underlying profiling tools such as the WCC compiler produced by the University of Hamburg [START_REF] Falk | A compiler framework for the reduction of worst-case execution times[END_REF]. Energy measurements are obtained by measuring the amount of energy in Joules (J) that is used by a complete processor package; i.e. we measure the total energy that is drawn by each hardware CPU socket. Energy results are obtained manually for the purposes of this paper, using Intel's Running Average Power Limit (RAPL) [START_REF] David | Rapl: Memory power estimation and capping[END_REF] system to collect this information, using model specific registers (MSR) to access the RAPL measurements. The MSRs provide accurate power readings for various systems components within each package e.g. the GPU and DIMMs. The same mechanism also allows energy consumption to be controlled/capped. We take the RAPL estimation of energy for the overall execution of the application. RAPL records power usage in terms of Watts (i.e. Joules per second). We calculate energy usage by computing the rate of change in power per unit of time using the formulae shown below:

Energy = Power × Time Joules = Watts × Seconds
1 available on Hackage at http://hackage.haskell.org/package/language-c Security encompasses many aspects of interest. Communication properties like confidentiality/secrecy [START_REF] Ryan | Mathematical models of computer security[END_REF] or integrity [START_REF] Clark | A comparison of commercial and military computer security policies[END_REF] of the sent/received data, or even vulnerability to the most powerful attacker [START_REF] Focardi | A uniform approach for the definition of security properties[END_REF], can be captured by information-flow policies [START_REF] Bell | Secure computer system: Unified exposition and multics interpretation[END_REF] or trace-based properties like non-interference [START_REF] Goguen | Security policies and security models[END_REF] to prevent covert channels (unintentional transmission of sensitive information by using intended communication channels). A side-channel is a way of transmitting information (purposely or not) to another system out of the standard (intended) communication channels. Side-channel attacks aim at breaking cryptography by exploiting information that is revealed by an algorithm's physical execution. For instance, observing execution time [START_REF] Kocher | Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems[END_REF] or power profile [START_REF] Kocher | Differential power analysis[END_REF] may reveal secret information. We focus on these time-and power-related security properties in Section 4.2, to emphasize the relations between these three non-functional properties. Another computational property is the vulnerability to faults [START_REF] Ziade | A survey on fault injection techniques[END_REF] injected during the execution in order to retrieve sensitive information from the alteration of the behavior of the program.

In this paper, we omit the details of obtaining such non-functional information, leaving it for future work to extend the Drive system with suitable linkage to automated tools (such as WCC [START_REF] Falk | A compiler framework for the reduction of worst-case execution times[END_REF]) to obtain the information automatically. However, our system infers the resource usage costs from a variety of underlying tools that are both dynamic and static, rather than performing static analysis on the source code itself. This gives the advantage of relying on real-world resource costs that are taken from actual measurements of time and energy from the execution profile of the application. Examples of such underlying tools are the AbsInt tool for instruction-level energy analysis [START_REF] Wilhelm | The worst-case execution-time prob-lem—overview of methods and survey of tools[END_REF], TimeWeaver for hybrid worst-case execution time analysis [START_REF] Kästner | TimeWeaver: A Tool for Hybrid Worst-Case Execution Time Analysis[END_REF], and WCC for worst-case timing analysis of C source code and static energy models, such as those provided by Eder et al. [START_REF] Morse | On the limitations of analysing worst-case dynamic energy of processing[END_REF].

ENERGY, TIME AND SECURITY CONTRACTS

Drive is a framework for forming contracts to support the inexperienced and possibly unskilled developer with the tools and techniques to reason about time, energy and security properties as first class citizens of the underlying language. Although Drive is, in theory, completely language independent, we demonstrate its effectiveness and generality on the C programming language, a language very commonly used for programming embedded systems. The workflow for using Drive is shown in Figure 1.

Starting with an original C source program, the programmer first annotates the source with annotations, by using a Contract Specification Language, a domain-specific language that extends C with special annotations and contract specification definitions (described in Section 4) describing non-functional properties of their source code and assertions (or contracts) around those properties. This annotated source code, with non-functional properties and assertions, is then passed through an ANSI C(99) parser (described in Section 2.2), which takes the annotated source code and produces a generated Idris model of the source code. This generated Idris model is a high-level abstract representation of the C program with its CSL annotations and assertions, which we pass to an underlying automated proof engine (also implemented in Idris) in order to verify that the programmer-defined certificate is valid or not. In addition to verifying the certificate, the CSL source code may be also passed to underlying tooling that may acquire further nonfunctional information about the execution of the application, such as timing, energy and security information. If the contracts are met, the result of the whole process is a certified C source program.

Motivating Example

Listing 1: Dijkstra C example, showing annotations in CSL We consider the Dijkstra algorithm as implemented in the Beebs [START_REF] Pallister | BEEBS: open benchmarks for energy measurements on embedded platforms[END_REF] benchmarks as a motivating example; an extract of the code is shown in Listing 1. In this example, the programmer requires a guarantee of the worst-case complexity of the algorithm, which is O(e log v), where e = number of edges and v = number of vertices. This is achieved by adding annotations to the source code calling various CSL functions. These CSL functions obtain various nonfunctional properties about the program's execution, such as worst and average case time, energy usage and even security information (illustrated in Section 4.2). This is information that is obtained from underlying profiling and modelling tools. When the program is executed, the CSL framework will automatically call the underlying tooling and assign the results of the profiling and/or analysis to the C variable that is passed as an argument to the CSL function. CSL annotations always immediately proceed a C statement (where a C statement can be any valid C statement) that is intended to Examples of these CSL annotations are shown in Listing 1, where the programmer has added two annotations to the program source. The annotation on Line 12, __csl_time_worst_iter(&comparison_time ); takes the average worst-case time metric for the loop defined immediately after, on Line 12, and assigns it to the regular C variable, comparison_time, which is defined, in the normal C fashion on Line 6; the average is calculated as the arithmetic mean over the loop iterations. The annotation on Line 31, __csl_time_worst(&time_spent) ;, takes the worst-case-execution-time (WCET) for the execution of the proceeding C statement on Line 32, and assigns it to the C variable, time_spent (defined on Line 6). This measurement is obtained by calling an underlying tool that calculates the worst case execution time and assigns the result to the C variable, time_spent. By assigning the values of the non-functional properties to regular C variables in this way allows the non-functional properties to become first-class properties of the C language itself: they can be used in the same way regular C variables can be used. This means they can be part of conditionals, loop bounds, etc.

Finally, the assertion of the complexity being an upper bound, is expressed as a contract in the program source. This contract is written as an assertion in the source code at Line 34 in Listing 1. This assertion is translated down into an underlying automated proof mechanism that generates a contract that the assertion holds for the given expression. In this paper, we use Idris as our proof mechanism, details of which are described in Section 5. In this example, the programmer states in the source code what the contract should be, by the statement, __csl_assert(time_spent <= (EDGES * log (NUM_NODES) )* comparison_time);. Here, EDGES and NUM_NODES are regular C variables that are defined in scope; log is the standard logarithmic function. The source code then passes through our CSL compiler: comprising an extended C parser, which parses the C and CSL constructs, and generating an Idris program that is then executed by the contract system. The code that is generated by the parser is shown in Listing 2. In the listing, the Idris definition, dijkstra, on Line 5, represents an abstract high-level model of the C program in Listing 1, except that all of the superfluous structural detail have been removed, leaving only the information that is required to assert the contract. In this case, the only information that is required to verify the assertion are the variables representing the C variables of the assertion, and any variables being assigned values of non-functional information. dijkstra_assert models the assertion, where p0 etc. are generated definitions. The types, MkAssertion etc. are described in more detail in Section 5.

Listing 3: Example Idris contract for Dijkstra showing verified assertion

1 ([("time_spent", 32933), ("NUM_NODES", 256), ("EDGES", 1026), (" comparison_time", 23)], 2[MkAssertion (LTE (Var "time_spent") 3

(Mul (Mul (Var "EDGES") (Log (Var "NUM_NODES"))) ( Var "comparison_time")) 4

(MkEvald (Var "time_spent") 32933) 5(MkEvald (Mul (Mul (Var "EDGES") (Log (Var " NUM_NODES"))) (Var "comparison_time")) 6

...

7

(Yes (LTESucc (LTESucc ... This generated Idris code is then passed to the Idris engine (described in Section 5), which produces a certificate, shown in Listing 3. In the listing, we see the result of verifying the assertion that was expressed in Listing 1 at Line 34 as a value in the DecEq type in Idris. Using DecEq gives us a decidable result as to whether the assertion holds for the given variables, or it does not. In Listing 3, we can see that, on Line 7, Idris returns Yes, indicating the assertion holds. This result is a certificate, proved correct by the underlying Idris type system.

CONTRACT SPECIFICATION LANGUAGE

The Contract Specification Language (CSL) is an Embedded Domain Specific Language (EDSL), allowing the programmer to annotate their source code in order to reason about non-functional properties as first-class citizens. CSL is both comprehensible to the programmer, and precise and detailed enough to support the required compiler optimisations and transformations. Therefore, CSL allows suitable annotations to be integrated into the program source, making it possible for the programmer and compiler to understand and reason about, e.g., energy, time, and security properties of the program. In order to illustrate the concept, we define CSL for C, but it can, in principle, be extended to other languages.

Expressing Time and Energy Properties

In order to express properties of time and energy, the programmer is required to annotate the source code with CSL annotations that make time and/or energy values available. Listing 4 shows the CSL annotations for assigning time values for a given statement, where annotations are defined as functions. These fall into three different aspects: worst-case (Line 1), best-case (Line 7), and average-case (Line 4) execution time. Each CSL annotation acts like a normal C function, where the parameter is a variable that is in scope. Each annotation must be placed before a regular C statement. Semantically, Listing 4: CSL time annotations the annotation provides a measurement for the non-functional metric of the proceeding statement. Intuitively, this is equivalent to an assignment.

Listing 5: CSL time example

1 double loop_time; 2 3 __csl_time_worst(&loop_time); 4 for(int i =0; i < BOUND; i++){ 5 f(i); 6 }
For example, in Listing 5, the for-loop (Lines 4-6) is annotated with __csl_time_worst(&loop_time) (Line 3) in order to obtain its worst-case execution time measurement. This value is stored in the variable, loop_time, which is passed by reference. The __csl_time_worst annotation will update the variable loop_time with the value of the metric measured.

Listing 6: CSL energy annotations Capturing energy measurements behaves in a very similar manner to capturing time measurements. Listing 6 shows the CSL annotations for assigning energy values. Similar to the time annotations of Listing 4, there are three possible annotations for energy: worstcase (Line 1), average-case (Line 4), and best-case (Line 7). These energy annotations also directly precede a C statement, capturing the measured energy measurement for the execution of that statement.

Listing 7: CSL example (revision 1)

1 double loop_time; 2 3 __csl_energy_worst(&loop_energy); 4 for(int i =0; i < BOUND; i++){ 5 f(i); 6 }
For example, we might modify Listing 5 to measure energy in instead of time by replacing the annotation on Line 3. The resulting code, in Listing 7, will assign loop_energy the measurement for the worst-case energy usage for the for-loop.

Listing 8: CSL accumulator annotations CSL can be further extended with measurement annotations by using an underlying tool capable of making such desired measurements. One useful set of annotations, for example, is for the purpose of measuring statements within a loop context. Listing 8 shows the CSL annotations for assigning time values for a given statement that is within the body of a loop. As before, there are three kinds: worst-case (Line 4), best-case (Line 7), and averagecase (Line 2). The worst-case annotation captures the worst time seen for stmt2 over all iterations of the loop. Similarly, the best-case annotation captures the best time seen for stmt3 over all iterations of the loop. Finally, the average-case annotation captures the mean average time of stmt1 over all iterations of the loop. For example, in Listing 9, we extend Listing 5 by adding an accumulator annotation.

Listing 9: CSL accumulator example Here, the annotation on Line 5 captures the average amount of time the f(i) operation on Line 6 takes for 0 < i < BOUND.

For all declaration annotations above, it is possible to change the default unit by supplying an optional string parameter that lets the programmer choose an appropriate unit to measure; e.g., in milliseconds, seconds, nanoseconds, for time, and joules and watts•seconds for energy. In our illustrative implementation, the default option for time is milliseconds and the default for energy is joules.

Expressing Security Properties

CSL annotations may be extended to non-functional properties other than time and energy. In order to illustrate this, we consider a small subset of security properties, with particular emphasis on side-channel attacks. We define three annotations in Listing 10 for capturing security levels for both side-channel attacks (Lines 1 Listing 10: CSL annotations for security properties and 4) and fault injection (Line 7). As in Section 4.1, security annotations act like a normal C function, where the parameter is a variable that is in scope. Each annotation is placed before a regular C statement. Semantically, the annotation provides a security level for the proceeding statement. For the purposes of this paper, the security level of a statement is obtained from a given tool, e.g. [START_REF] Reparaz | Dude, is my code constant time? In: Design[END_REF] for time, that inspects how secure the code is for that particular property, and for a produced binary on a given architecture. Here, we assume that the security level is expressed as an integer.

In order to demonstrate these annotations/properties, we consider variants computing the (left-to-right) modular exponentiation by squaring, which is commonly used in, e.g., RSA [START_REF] Rivest | A method for obtaining digital signatures and public-key cryptosystems[END_REF]. They return the result of a k mod n computed with an accumulator, x, where a and n are public variables, and k is some secret key.

Listing 11: Security Example: Square-and-Multiply

1 int sqmul(int a, unsigned int k, int n) { 2 int x = 1; 3 for (int i = 8*sizeof(int) -1 ; i >= 0 ; i--) { 4 x = x*x % n; 5 if ((k >> i) & 1) { 6 x = x*a % n; 7 } 8 } 9 return x; 10 }
The condition of the if-statement on Line 5 detects the value of the i th bit of the secret k, expressed in binary form. For every iteration, Listing 11 computes the multiplication only if that bit is a 1, which can be detected by observing execution time [START_REF] Kocher | Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems[END_REF] or a power profile [START_REF] Kocher | Differential power analysis[END_REF], and thus leads to information leakage from both time and power side-channel attacks.

Listing 12: Square-and-Multiply-Delay The CSL annotation for time side-channel attacks from Listing 10 can be used to measure calls to both sqmul and sqmul_delay, as in Listing 13, where we would expect that sqmul_delay returns a higher security level than the call to sqmul. However, this is not necessarily the case for power profiles, that can be read (Simple Power Analysis [START_REF] Kocher | Differential power analysis[END_REF]) in order to detect whether or not a multiplication has been computed during an iteration. In order to mitigate this, another variant of the square-and-multiply function might be employed.

1 int sqmul_delay(int a, unsigned int k, int n) { 2 int x = 1; 3 for (int i = 8*sizeof(int) -1 ; i >= 0 ; i--) { 4 x = x*x % n; 5 if ((k >> i) &
; i--) { x = x*x % n; if ((k >> i) & 1) { x = x*a % n; } else { y = x*a % n; } } return x; }
Here, a dummy variable, y, is introduced and both branches of the if -statement perform the same operations. Similar to the time-based security level in Listing 13, security levels based on power profiles can be measured using the annotation in Listing 10. Here, security levels are stored in both sec_lvl_power_delay and sec _lvl_power_always, where we would normally expect the security level for sqmul_always to be greater than sqmul_delay. But the multiplication in the else branch of Listing 14 is a dummy operation, so injecting a fault [START_REF] Ziade | A survey on fault injection techniques[END_REF] in x*a % n will change the final result only if the current secret bit is 1, thus leaking information. This is not the case with the Montgomery Ladder [START_REF] Joye | The montgomery powering ladder[END_REF] where both variables x and y are interleaved accumulators. In Listing 16, a fault injected will propagate through successive iterations, so will alter the final result irrespective of the value of the current secret bit, preventing the opponent to obtain secret information. The security level of statements against fault-injection may be captured by the corresponding annotation in Listing 10.

Listing 16: Montgomery Ladder Similar to Listings 13 and 15, Listing 17 demonstrates the faultinjection-based annotation, capturing security levels for calls to sqmul_always and montgomery_ladder. Here, we would expect the security level of montgomery_ladder to be greater than sqmul_always.

1 int montgomery_ladder(int a, unsigned int k, int n) 2 { 3 int x = 1; 4 int y = a; 5 for (int i = 8*sizeof(int) -1 ; i >= 0 ; i--) { 6 if ((k >> i) & 1) { 7 x = x*

Assertions

Assertions in CSL allow programmers to express contracts about their programs over the variables defined within it; e.g. the comparisons between security levels in Section 4.2. These variables may be used to capture non-functional properties of, e.g., time, energy, and security, as described in this section, or they may be normal variables that are in scope in the language for which CSL is defined. The assertion is checked using the model described in Section 5. An assertion takes the following form.

Here, bool_expression is an expression that returns a boolean value. The exact definition of well-formed expressions is derived from the underlying model since it is the model that determines whether the assertion holds, for a given context. In our exemplar __csl_assert( bool_expression ); implementation, this is a simple expression language comprising basic arithmetic operators and the binary operations: conjunction, disjunction, equality, and the standard inequalities over numbers. This may be extended to allow more complex expressions, given an extended model and/or parser (Section 2.2).

In order to demonstrate the use of assertions, we extend Listing 9.

Listing 18: CSL time example Here, loop_time <= (iter_time * BOUND) is a normal boolean C expression. loop_time, iter_time and BOUND are all variables that are in scope and contain values at the point of the assertion. The programmer can call __csl_assert at any point in her C program, provided the free variables within the boolean expression are in scope and have values assigned to them. Assertions regarding security properties are expressed similarly. For example, given the square-and-multiply functions in Listings 11 and 12, we might extend Listing 13 with an assertion. Here, the security levels of the two function calls for time sideint sec_lvl_time, sec_lvl_time_delay; __csl_security_sca_time(&sec_lvl_time); int x = sqmul(a, k, n); __csl_security_sca_time(&sec_lvl_time_delay); int y = sqmul_delay(a, k, n); __csl_assert(sec_lvl_time <= sec_lvl_time_delay); channel attacks are captured in sec_lvl_time and sec_lvl_time_delay by the annotations on Lines 4 and 7, respectively, and the assertion is the simple inequality, sec_lvl_time <= sec_lvl_time_delay.

Energy, Time and Security Properties as First-class Citizens

An advantage to our approach is that lifting these non-functional properties to the source level makes them first-class citizens of the source language. This means that if the programmer annotates their C source code with time, energy and security properties, these properties are assigned to standard C variables, and can be used in the usual way C variables can. For example, in the listing below, the programmer uses CSL to obtain the energy usage of a simple loop, and then following the loop, the energy usage is used in an if statement. Here, loop_energy is obtained by calling the CSL construct at Line 1 in the expected way, and then used, in Line 6, as part of an if statement. Here, loop_energy is checked to make sure that it does not exceed 20 joules of energy, executing different secure algorithms depending on the value of loop_energy as a result of the comparison.

CONTRACT DEFINITION AND DERIVATION

An annotated C program is modelled using Idris in order to determine whether assertions within the program hold. Models of programs are automatically derived using the parser from Section 2.2 and are inhabitants of the type CLang.

Listing 19: Idris model type CLang abstracts away all aspects of the annotated C program aside from CSL assertions and the assignments of variables used in those assertions; denoted respectively by Assert, BlockTime, BlockEnergy and DecVar. Variables, x, in models are unique and represent only the value that is live within the assertion. All values are modelled using natural numbers (Nat) to facilitate proof derivation; extending this to other types is a concern for future work. Where variables are not natural numbers in the original program, it is currently left to the parser (Section 2.2) to denote those original values consistently into natural numbers. Models are in continuation passing style, where, as is standard, k denotes the continuation, and Halt denotes the end of a continuation. For example, the assertion __csl_assert(x > 12);, when x = 13, can be modelled as 1 DecVar "x" 13 (Assert asn Halt)

where asn is a function that models the assertion x > 12.

Assertions are boolean expressions that have a truth value, expressed via type inhabitance. Models can be constructed that contain assertions that do not hold. This allows a report to be presented to the programmer detailing whether, and how, each assertion holds. Since assertions are likely to have free variables, the model must specify a context, Env, via the function argument to the Assert constructor, that provides definitions for those variables (Listing 19, Line 5, asn : Env -> Assertion). Contexts are defined as a mapping of variable names to values; e.g. here, Env = List (String,Nat). Proof terms of assertions are constructed by computing the normal forms of assertions; contexts provide definitions for free variables in assertions, allowing this. For example, in Listing 2, the variables in dijkstra_assert are substituted for their values by lookup in env, which is generated from definitions in the rest of the model, dijkstra. The type of assertions, Assertion (Listing 19, Line 5), is effectively a type alias for the type of boolean expressions, BooleanExpression. Boolean expressions comprise conjunction (And) and disjunction (Or) over boolean expressions, and equality (Eq) and (≤) (LTE) operations over natural numbers. Semantically, these functions are defined in the usual way. Our implementation includes the other standard inequality operators, but these are omitted here for clarity, since they can be defined in terms of (≤).

Listing 20: Assertion and boolean expressions definition

Under our representation in Listing 20, each boolean expression is a binary operation, with arguments denoted x and y. Boolean expressions are extended with proof terms, xNF and yNF, for the relations BEvald and Evald, and the truth value for the expression, prf. Both xNF and yNF relate, depending on the operation, boolean or numeric expressions with their normal forms. We say BEvald x x ', where x is a boolean expression and x' is the boolean (Bool) to which x evaluates; and Evald x x', where x is a numeric expression (Listing 21) and x' is the natural number (Nat) to which x evaluates. The truth term for the corresponding predicate, prf, is defined using the decidable proposition (Dec) and an underlying proposition that reflects the operation. For example, the truth value of And (Listing 20, Line 9) has the type Dec (TyAnd x' y'), where TyAnd is a type representing logical conjunction. When And evaluates to True, prf = Yes prf', where prf' is a constructive proof that TyAnd x' y' is 1 data TyAnd : Bool -> Bool -> Type where 2 MkAnd : TyAnd True True inhabited for the given x' and y'. For example, given prf : TyAnd True True, prf = Yes MkAnd). Similarly, when And evaluates to False, prf = No prf', where prf' is proof that the underlying proposition, TyAnd x' y', would be a contradiction (i.e. is uninhabited) for the given x' and y'.

Both equality and (≤) operations range over numeric expressions, comprising literal values (Lit), variables (Var), addition (Add), subtraction (Sub), multiplication (Mul), truncated division (Div), the truncated logarithm to base 2 (Log), and the modulo operation (Mod). Nothing => 0 17 eval env (Plus x y) = (eval env x) `plus`(eval env y) 18 eval env (Sub x y) = (eval env x) `minus`(eval env y) 19 eval env (Mul x y) = (eval env x) `mult`(eval env y) 20 eval env (Div x y) = assert_total $ (eval env x) `div`(eval env y) 21 eval env (Mod x y) = assert_total $ (eval env x) `mod`(eval env y)

Boolean expressions are reduced to a boolean value (beval) by discriminating on prf. Numeric expressions are reduced to a natural number (eval) by denoting each NumericExpression operation into the respective Idris prelude function over natural numbers. Variables (Var, Lines 14-16) are looked up in the context, env, by the list prelude function lookup. The definition and generation of the Idris model require that all free variables in assertions are defined in the context. Consequently, the Nothing branch (Line 16) will, by definition, never be reached, but is included because lookup returns a Maybe value and eval returns a Nat. In the future, we intend to reflect this property in the type, obviating the need for lookup. Similarly, the arithmetic operations Log, Div, and Mod require assert_total to ensure evaluation to normal form, since the respective Idris prelude functions, log, div, and mod, are partially defined. We ensure that only models for which there are defined instances of log, div, and mod are generated. In principle, it is possible to guarantee within the system that, for those cases, only arguments for which there are defined behaviours may be constructed, obviating the use of assert_total.

Reporting the Contract. For each model, the context and list of assertions are derived using the function mkAssertions : CLang -> List Assertion. mkAssertions is a fold over a model, whose step function collects assertions from Assert constructors, and variables and values from BlockTime, BlockEnergy, and DecVar constructors. Construction of the list of assertions requires a proof of whether each assertion holds, which is derived automatically via the reduction functions beval and eval, in conjunction with decision procedures for each boolean expression that is introduced via model generation. Decision procedures comprise: isAnd for conjunction; isOr for disjunction; decEq from the Idris prelude for equality; and isLTE from the Idris prelude for (≤). In order to illustrate this process, we consider the model defined in abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] constructor, the step function passes the above context, env, to the assertion function, dijkstra_assert. Since Idris is strictly evaluated, this will cause the normalisation of p0 and p4, producing p0' = 32933 and p4' = 188784, respectively, via the (eval env) (partially applied) function. The LTE constructor requires a value of type Dec (LTE p0' p4), which is provided by the evaluation of the term (isLTE p0' p4'), or (isLTE 32933 188784), substituting the values of both p0' and p4'. In this example, the prelude function, isLTE, is used to provide a value that inhabits the type Dec (LTE p0' p4). Under the Curry-Howard correspondence and Intensional Type Theories [START_REF] Slama | Automatically proving equivalence by type-safe reflection[END_REF] upon which Idris is based, the type Dec (LTE p0' p4) is a proposition and the result of (isLTE 32933 188784) is a proof of that proposition, and thus a proof of the assertion itself. Accordingly, we say that the result of the abstract evaluation of dijkstra is a mechanical proof of the assertions therein, where Idris is used as a proof assistant.

EVALUATION

We provide our experimental system setup and describe our evaluation results.

Experiment Setup

For our experiments we evaluate across two different machines.

The first set of experiments, corryvreckan, are conducted on a server with Intel Xeon E5-2690 CPU with 28 cores, running at 2.6 Ghz with 256 GB of RAM, with the Scientific Linux 6.2 operating system with gcc 4.8.5 with optimisations turned off. The second set of experiments, raspberrypi, are executed on a Raspberry Pi Model 3 B, Quad-core 1.2Ghz Broadcom BCM2837 64bit CPU with 1 GB of RAM, with Raspbian GNU Linux (9) and gcc 6.3.0 with optimisations turned off.

The Beebs Benchmarks

For purposes of our evaluation, we use the Beebs benchmarks, which are designed for evaluating WCET and energy analysis for embedded systems [START_REF] Pallister | BEEBS: open benchmarks for energy measurements on embedded platforms[END_REF]. In this paper, we chose a subset of the sorting algorithms from Beebs, where we measured the theoretical worse-case execution time based on the worst-case complexity of the sorting algorithm. For each sorting algorithm we annotated the source-code with CSL contructs measuring the average comparison time of the sorting algorithm, together with the total sorting time for the given input. The CSL assertion then asserts that the theoretical upper-bound (calculated from the average comparison time and the worst-case complexity) is indeed an upper bound for the given Beebs input data. In all cases, the contract system verifies that the worst-case is indeed an upper bound.

Experiments on corryvreckan

Our experiments for corryvreckan are summarised in Figure 3 array size) of the given Beebs benchmark data, the calculated worstcase complexity of the algorithmn, the average operation (or comparison) time for the algorithm (measured using monotonic clock time, in milliseconds), the worst-case theoretical time, based on the worse-case complexity and the average operation time, the number of operations performed in the benchmark, and the total Beebs time. For each benchmark, we show that the worst-case time is an upper bound on the total runtime. In Figure 2(a), we show a summary of the corryvreckan results as a bar chart. Here, the y-axis is showing a logarithmic scale of milliseconds. The blue bar shows the actual time, and the red bar shows the theoretical worst-case time based on the average operation time and the worst-case complexity of the algorithm; in all cases the actual time is below the theoretical worst-case time. In all cases, the actual time does not exceed the worst-case time. For mergesort-asc and mergesort-equal, there were 0 operations performed due to the input lists already being sorted; we omit their results here.

Experiments on raspberrypi

Our experiments for the raspberry pi proceed in a similar manner to those shown for corryvreckan, and are given in Figure 4. The Raspberry Pi is a small embedded device, no untypical of the types of devices found in embedded systems. It allows us to model the benchmarks in an embedded system, in contrast to the multicore system, corryvreckan, and show the applicability of the Drive system to an embedded space. The benchmarks were executed in a similar manner to those for corryvreckan, with the same data inputs as supplied by the Beebs benchmarks. Again, mergesort-asc and mergesort-desc have 0 operations, so complete in almost 0 time; we again omit their results. We omit details of dijsktra and select for the Raspberry Pi due to segmentation faults in the executions. A comparison of the Beebs actual times (shown in blue) versus the theoretical worst-case time (shown in red) are given in Figure 2(b).

RELATED WORK

There is a great deal of work within the programming language community on the calculation and bounding of resource usage, generally with a focus on memory usage or worst-case execution time [START_REF] Çiçek | Refinement types for incremental computational complexity[END_REF][START_REF] Wilhelm | The Worst-case Execution-time Prob-lem&Mdash;Overview of Methods and Survey of Tools[END_REF]. Programming language approaches typically seek to allow the programmer to reason about resources at the type level, inter alia. Approaches include: the use of abstract interpretation to infer symbolic bounds [START_REF] Gulwani | SPEED: precise and efficient static estimation of program computational complexity[END_REF]; the use of amortised analyses to automatically infer polynomial multivariate bounds [START_REF] Hoffmann | Multivariate amortized resource analysis[END_REF]; the use of refinement types to ensure that successive iterations cost less than previous iterations in incremental computing [START_REF] Çiçek | Refinement types for incremental computational complexity[END_REF]; the use of linear dependent types to bound the number of reductions that may be applied [START_REF] Lago | The geometry of types[END_REF]; and, similarly, the use of sized types to analyse space usage [START_REF] Chin | Calculating sized types[END_REF][START_REF] Hughes | Recursion and dynamic data-structures in bounded space: Towards embedded ML programming[END_REF][START_REF] Vasconcelos | Inferring cost equations for recursive, polymorphic and higher-order functional programs[END_REF]. Where these approaches generally operate within specific type systems or languages, applying them to other languages, e.g. C, would typically be a substantial task. Whilst a model of some program in the given target language could be constructed, these analyses would result in an analysis of the model,

BEEBs Example

BEEBs Input Size Worst-case compl. Avg. Op. Conversely, the approach presented here uses concrete resource information derived from the original program, thereby allowing us to reason about the original program itself and in a manner that directly and accurately reflects resource usage.

Beyond time and space, recent work has exposed the energy consumption of a program in the form of a function that is parameterised by program arguments [START_REF] Georgiou | Energy transparency for deeply embedded programs[END_REF][START_REF] Liqat | Energy consumption analysis of programs based on XMOS isa-level models[END_REF]. Security aspects, such as information flow and leakage, have also been modelled using type systems [START_REF] Chen | A permission-dependent type system for secure information flow analysis[END_REF][START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. As additional non-functional properties become of interest, it becomes increasingly relevant to combine or compose said properties when reasoning about them in the program. To the best of our knowledge, existing approaches are generally limited to a single resource. The few approaches that do trade energy requirements with performance constraints [START_REF] Andrei | Quasistatic voltage scaling for energy minimization with time constraints[END_REF][START_REF] Xian | Energy-aware scheduling for real-time multiprocessor systems with uncertain task execution time[END_REF], with one notable exception [START_REF] López-García | Interval-based resource usage verification by translation into horn clauses and an application to energy consumption[END_REF], treat both properties as a constraint within the compilation/optimisation stage, and do not allow the programmer to reason about them. Conversely, and since the approach presented here builds upon, and uses, existing tools, it is both possible and simple to express assertions about multiple non-functional properties at the program level.

The aforementioned notable exception, the Ciao Preprocessor system (CiaoPP) [START_REF] Hermenegildo | Integrated program debugging, verification, and optimization using abstract interpretation (and the ciao system preprocessor)[END_REF][START_REF] López-García | Interval-based resource usage verification by translation into horn clauses and an application to energy consumption[END_REF][START_REF] Serrano | Resource usage analysis of logic programs via abstract interpretation using sized types[END_REF], enables the programmer to infer resource usage, and reason about the correctness of programs with respect to resource usage information. CiaoPP achieves this by translating annotated programs in high-level languages, e.g. Java [START_REF] Gosling | The Java Language Specification, Java SE 8 Edition[END_REF] and XC [1], into sequences of Horn clauses. This Horn Clause Intermediate Representation (HC IR) is used to reason about (the correctness of) transformations over the global state of the program. Despite the apparent similarities of both Drive and CiaoPP systems, beyond the choice of model representation, there are three distinct differences:

(1) the approach to resource analysis;

(2) the exposure of resource usage information to the programmer; and, (3) the scope of the respective models.

CiaoPP uses its HC IR to derive resource usage information: reporting static resource analyses for both time and energy [START_REF] López-García | Interval-based resource usage verification by translation into horn clauses and an application to energy consumption[END_REF], and memory and the transmission of bits [START_REF] Serrano | Resource usage analysis of logic programs via abstract interpretation using sized types[END_REF]. To the best of our knowledge, no security analyses have thus far been a subject of CiaoPP resource usage analysis. The use of external tooling in Drive represents a trade-off between the tightness of integration and assurances, as seen in CiaoPP, and an increased flexibility in choice of approaches to resource analyses. External tooling need not be limited to the use of a specific representation, but different tools may instead use their own internal representation, potentially allowing a wider range of analyses. However, external tooling must generally be trusted by the programmer, where trust might be derived from, i.e., empirical testing or external proofs.

The resource analyses available within the CiaoPP system return functions that take the size of relevant data as an argument. Conversely, the Drive system expects ground values for specific instances of the annotated statement. Moreover, unlike Drive, CiaoPP does not reflect resource usage values into the original program and thus this information cannot be used in a first-class way. Whilst it should be noted that the underlying Ciao does facilitate first-class resource usage values, CiaoPP does not propagate those values back into the original language [START_REF] López-García | Interval-based resource usage verification by translation into horn clauses and an application to energy consumption[END_REF].

Beyond resource analysis, the scope and approach to verification represents a significant difference between the two approaches. CiaoPP models the (concrete and intended) semantics of a given program written in a annotated high-level language using the HC IR, in part to facilitate its resource analyses. Conversely, Drive models only those parts of the program that are necessary for determining validity of CSL assertions; in part, facilitated by the use of external tools. The certificates derived from these models represent proofs by reflection or contradiction of whether an assertion holds. Drive can thus be seen as a proof-carrying approach [START_REF] Necula | Proof-carrying code[END_REF], where the certificates are checkable by the Idris type checker. CiaoPP similarly provides the fixpoint computed by the preprocessor [START_REF] Albert | Certificate size reduction in abstraction-carrying code[END_REF]. Due to the nature of the CiaoPP analysis, these fixpoints may become large as the program itself grows larger. Whilst the certificates produced by the Drive system are focussed on assertions and carry minimal information, due to the constructive nature of proofs in Idris, and the use of natural numbers in Drive, large numbers may produce large certificates. Future work will focus on making these proofs smaller, easier to read and understand, and investigate making these proofs first-class; i.e. accessible within the program being analysed. One consequence of the relative immaturity of the technique, is that the assertion language supported by CiaoPP is more expressive than that which is supported by Drive. Future work will consider increasing the expressiveness of the Drive assertion language; for example, allowing the inference of intervals for free variables in non-ground assertions.

Measurement and Inference of Resource Usage. The approach presented here is dependent upon other tools, e.g. the WCET-aware C Compiler [START_REF] Falk | A compiler framework for the reduction of worst-case execution times[END_REF], in order to provide resource usage values to the model. Unsurprisingly, the worst-case execution time (WCET) community has been a significant driver of such tools; a general overview of methods and tools is provided by Wilhelm et al. [START_REF] Wilhelm | The Worst-case Execution-time Prob-lem&Mdash;Overview of Methods and Survey of Tools[END_REF]. For example, one of the more popular methods used for WCET analysis is the Implicit Path Enumeration Technique, introduced by Li et al. [START_REF] Li | Performance analysis of embedded software using implicit path enumeration[END_REF], which estimates best-and worst-case times for embedded software without needing to enumerate all possible control-paths in a program.

Energy usage is of increasing interest due to the prevalence of battery-powered systems. The measurement of energy usage typically comes in three forms: 1) instruction set models for simple, usually predictable, embedded architectures [START_REF] Kerrison | Energy modeling of software for a hardware multithreaded embedded microprocessor[END_REF][START_REF] Tiwari | Power analysis of embedded software: a first step towards software power minimization[END_REF]; 2) hardware performance counter models that utilise more complex architectures' performance events (e.g. cache misses and branch misspredictions) [START_REF] Shao | Energy characterization and instruction-level energy model of intel's xeon phi processor[END_REF]; and 3) the use of linear regression on an amount of empirical data to extract unknown terms that can be utilised to construct an energy model [START_REF] Núñez-Yáñez | Enabling accurate modeling of power and energy consumption in an arm-based system-on-chip[END_REF].

Regarding security properties, in [START_REF] Di Pirro | Ensuring information security by using haskell's advanced type system[END_REF] the authors used Haskell's type system to enforce secure information flow (non-interference [START_REF] Goguen | Security policies and security models[END_REF]), augmented with flexible declassification policies, and secure computation on untainted data (both verified if the source code compiles), and mandatory user input validation (verified at runtime). Their lightweight Haskell library for writing and reading files ensures that values in sensitive applications come from a trusted source of input, and provides a simple way for formalizing declassification policies. But the programmer is forced to validate every untrusted value and to provide two different paths (whether an error occurs or not) in the source code, while in our paper we are making no assumption on the developer behaviour.

FABLE [START_REF] Swamy | Fable: A language for enforcing user-defined security policies[END_REF] is a core formalism for a programming language in which programmers can 1) define custom security labels and associate them with the data they protect using dependent types, and 2) define the interpretation of labels in special enforcement policy functions separated from the rest of the program. This allows to write programs that enforce a variety of security policies, not restricted as above to information flow security policies, such as access control, static and dynamic information flow with forms of declassification, provenance tracking and policies based on security automata. FABLE does not guarantee that a security policy is correctly implemented, but its design simplifies proof of this fact.

As shown by both frameworks, in the literature the focus is on communication security properties like confidentiality/secrecy [START_REF] Ryan | Mathematical models of computer security[END_REF] or integrity [START_REF] Clark | A comparison of commercial and military computer security policies[END_REF] of the data. The security examples, properties and contracts expressed in this paper are more focused on preventing information leakage from the computation itself (side-channel attacks and fault injection). Our approach is more general because it does not rely on particular primitives to express security properties.

Another general approach is LOCKS [START_REF] Kumar | Locks: A property specification language for security goals[END_REF], which is a generic and formal DSL (domain specific language) that allows a security practitioner to express and compose (both qualitative and quantitative) security goals (embracing a wide number of attributes such as cost, damage, probability, etc.) in a declarative manner. These goals are expressed as queries over an attack model, the SAM (structural attack model), which is based on partially ordered sets of successful attacks that dictates which steps needs to be carried out and in which order, and is used as the semantic model for LOCKS. These security goals can be compared to the (more accessible) regular C expressions that we used for the assertions, and thus LOCKS can be compared to Drive. But they lack an automated tool like Idris to verify whether these goals are achieved or not.

CONCLUSIONS AND FUTURE WORK

In this paper, we presented a novel framework, called Drive, allowing the programmer to reason about Energy, Time and Security (ETS) properties of their source-code. Moreover, Drive allows the programmer to express these ETS properties as first-class properties of the underlying language. We also introduced a new DSL, called the Contract Specification Language (CSL) to allow programmers to annotate the C source-code with ETS properties and source-level provable contracts. These source-level contracts are verified by an underlying type system that models the high-level structures of the source-code, giving a decidable proof that the contract has been met. This is used to allow the programmer to, for example, place upper bounds on sections of their source code in terms of e.g. time and energy, or define a security level that they require to be met. We evaluated our approach using a set of sorting algorithms from the Beebs benchmarks suite, on a 28-core multi-core machine and a raspberry pi model 3 B. Both results allowed us to evaluate our framework on showing that the worst-case complexity of the sorting algorithms is indeed an upper-bound for the supplied Beebs benchmarks data sets.

In the future, we plan to extend our work in a number of new directions.

• We intend to make contexts parameters of the assertion type, define models such that variables carrying proofs of their inclusion in the context, and avoid the use of partial definitions for arithmetic operations. This will obviate the need for evaluation relations and an explicit lookup operation. • We will extend the assertions to be able to take into account open terms. For example, the contract may be verified correct depending upon some assumption.

• We plan to extend our type-system to model the source code using a small-step semantics; this would enable us to model and verify assertions based on user-defined functions. • We will evaluate our technique on a number of examples that are dependent on the energy consumption of the application w.r.t to the total energy budget of the device. For example, modelling the Beebs benchmarks on a small embedded device, such as the Discovery STM32. • We plan to extend our framework on security contracts, including evaluating over a number of security benchmarks, testing security attacks such as side-channel attacks, etc.

Figure 1 :

 1 Figure 1: The Drive framework for producing contracts of non-functional properties of C programs

Listing 14 :

 14 Square-and-Multiply-Always int sqmul_always(int a, unsigned int k, int n) { int x = 1; int y; for (int i = 8*sizeof(int) -1 ; i >= 0

Listing 15 :

 15 Square-and-Multiply Comparison: Power SCA int sec_lvl_power_delay, sec_lvl_power_always; __csl_security_sca_power(&sec_lvl_power_delay); int x = sqmul_delay(a, k, n); __csl_security_sca_power(&sec_lvl_power_always); int y = sqmul_always(a, k, n);

1

  data CLang : Type where 2 --CSL 3 BlockTime : (x : String) -> (v : Nat) -> (k : CLang) -> CLang 4 BlockEnergy : (x : String) -> (v : Nat) -> (k : CLang) -> CLang 5 Assert : (asn : Env -> Assertion) -> (k : CLang) -> CLang 6 --C Structures 7 DecVar : (x : String) -> (v : Nat) -> (k : CLang) -> CLang 8Halt : CLang

Listing 21 :Listing 22 :

 2122 Numeric expressions definition 1 data NumericExpression : Type where 2 Lit : (n : Nat) -> NumericExpression 3 Var : (x : String) -> NumericExpression 4 Log : (x : NumericExpression) -> NumericExpression 5 Plus : (x : NumericExpression) -> (y : NumericExpression) -> NumericExpression 6 Sub : (x : NumericExpression) -> (y : NumericExpression) -> NumericExpression 7 Mul : (x : NumericExpression) -> (y : NumericExpression) -> NumericExpression 8 Div : (x : NumericExpression) -> (y : NumericExpression) -> NumericExpression 9 Mod : (x : NumericExpression) -> (y : NumericExpression) -> NumericExpression Semantically, these functions are defined in the usual way. Values of both BooleanExpression and NumericExpression are denoted into their corresponding Idris prelude functions via beval and eval, respectively. Evaluation functions for boolean and numeric expressions 1 beval : (env : Env) -> (b : BooleanExpression) -> Bool 2 beval env (And x y xNF yNF (Yes prf)) = True 3 beval env (And x y xNF yNF (No contra)) = False 4 beval env (Or x y xNF yNF (Yes prf)) = True 5 beval env (Or x y xNF yNF (No contra)) = False 6 beval env (Eq x y xNF yNF (Yes prf)) = True 7 beval env (Eq x y xNF yNF (No contra)) = False 8 beval env (LTE x y xNF yNF (Yes prf)) = True 9 beval env (LTE x y xNF yNF (No contra)) = False 10 11 eval : (env : Env) -> (e : NumericExpression) -> Nat 12 eval env (Lit n) = n 13 eval env (Log n) = assert_total $ log2 (eval env n) 14 eval env (Var name) = case lookup name env of 15 Just value => value 16

Listing 23 :

 23 This represents anListing 23: The Idris Abstract Model dijkstra : CLang dijkstra = BlockTime "comparison_time" 23 $ DecVar "EDGES" 1026 $ DecVar "NUM_NODES" 256 $ BlockTime "time_spent" 32933 $ Assert dijkstra_assert $ Halt dijkstra_assert : Env -> Assertion dijkstra_assert env = let p0 = (Var "time_spent") p0' = eval env p0 p1 = (Var "EDGES") p1' = eval env p1 p2 = (Var "NUM_NODES") p2' = eval env p2 p3 = (Var "comparison_time") p3' = eval env p3 p4 = (Mul (Mul p1 (Log p2)) p3) p4' = eval env p4 in MkAssertion $ LTE p0 p4 (MkEvald p0 p0') (MkEvald p4 p4') (isLTE p0' p4')

  . In the figure, we show for each benchmark, the input size (i.e. Comparison of Beebs runtimes versus worst-case on corryvreckan Comparison of Beebs runtimes versus worst-case on raspberrypi

Figure 2 :

 2 Figure 2: Comparison of Beebs runtimes versus worst-case theoretical bounds

  Listing 12 is less vulnerable to time side-channel attacks because the imbalance in execution time of the if-statement branches has been addressed by introducing a delay in the else branch. time_mult is the average execution time for the multiplication operation in the then branch, obtained by using (Line 6) the time-capturing annotation

	__csl_time_average_iter.
	Listing 13: Square-and-Multiply Comparison: Time SCA
	int sec_lvl_time, sec_lvl_time_delay;
	__csl_security_sca_time(&sec_lvl_time);
	int x = sqmul(a, k, n);
	__csl_security_sca_time(&sec_lvl_time_delay);
	int y = sqmul_delay(a, k, n);
		1) {
	6	__csl_time_average_iter(&time_mult)
	7	x = x*a % n;
	8	} else {
	9	delay(time_mult);
	10	}
	11	}
	12	return x;
	13 }

  of the original annotated C program in Listing 1; mkAssertions represents the abstract execution. Operationally, it folds over dijkstra, constructing the context: At an Assert

	1 env : Env
	2 env = [("comparison_time",23)
	3	,("EDGES",1026)
	4	,("NUM_NODES",256)
	5	,("time_spent",32933)]

  Time # BEEBs Ops Worst-case time BEEBs time Experiments on corryvreckan. Times shown in milliseconds.

	dijkstra	10	(v 2 ) + (e + v) log v	0.000227	220	0.0536	0.02599
	bs	15	log n	0.000333	3	0.00130099	0.000999
	bubblesort	100	n 2	0.0000869	5050	0.86	0.831
	insertsort	11	n 2	0.00009	9	0.0109	0.00099
	mergesort-pathological	100	n log n	0.0000784	51	0.521	0.004
	mergesort-random	100	n log n	0.00011728	486	0.0779	0.057
	mergesort-mostdesc	100	n log n	0.00006811989	367	0.045257	0.0249
	mergesort-mostasc	100	n log n	0.0001016949	59	0.06756	0.006
	mergesort-desc	100	n log n	0.000101124	356	0.0671	0.036
	mergesort-jittered	100	n log n	0.00022	9	0.1476	0.00199
	mergesort-mosteq	100	n log n	0.0000716	405	0.04757	0.029
	mergesort-worst	100	n log n	0.000111	522	0.07382	0.058
	qsort	20	n 2	0.0000625	16	0.0249	0.001
	select	20	n 2	0.00005882	34	0.0235	0.001
	Figure 3: BEEBs Example BEEBs Input Size Worst-case compl. Avg. Op. Time # BEEBs Ops Worst-case time BEEBs time
	bs	15	log n	0.00099	3	0.00386782	0.0030
	bubblesort	100	n 2	0.0003599	5050	3.5999	0.0759
	insertsort	11	n 2	0.00018	9	0.022	0.00699
	mergesort-pathological	100	n log n	0.00043137	51	0.28659	0.0219
	mergesort-random	100	n log n	0.000434	486	0.293	0.21
	mergesort-mostdesc	100	n log n	0.0004	367	0.293	0.1619
	mergesort-mostasc	100	n log n	0.00033	59	0.225	0.02
	mergesort-desc	100	n log n	0.000469	356	0.31166	0.167
	mergesort-jittered	100	n log n	0.00088	9	0.59	0.008
	mergesort-mosteq	100	n log n	0.000434	405	0.288	0.1759
	mergesort-worst	100	n log n	0.000469	522	0.31182	0.24499
	qsort	20	n 2	0.000312	16	0.125	0.00499
		Figure 4: Experiments on raspberry pi. Times shown in milliseconds
	not the original program. Moreover, as static approaches, these do
	not necessarily reflect actual execution times since architectural
	aspects (e.g. caching) are not modelled within the (type) system.

ACKNOWLEDGEMENTS

We thank Annelie Heuser and Tania Richmond for their help regarding side-channel analysis and the Montgomery ladder.

This work was supported by the EU Horizon 2020 project, Team-Play (https://www.teamplay-h2020.eu), grant number 779882, and UK EPSRC Discovery, grant number EP/P020631/1.