dataesr/scientific-paragraphs-categorization huggingface dataset:
The index i is used to separate multiple instances of MACs; for instance, it prevents calls to extend an accumulator with the wrong key. Our type-based separation between different kinds of elements is purely static. At runtime, the accumulator, and probably the key, are just bytes on the stack (or in registers), whereas the calls to add and mul are also likely to be have been inlined in the code that uses MACs. The newAcc function creates a new buffer for a given index, initialized to 0. The function returns a pointer to the buffer it allocates. The StackInline effect indicates that the function does need to push a frame before allocation, but instead allocates in its caller's stack frame. KreMLin textually inlines the function in its caller's body at every call-site, ensuring that the allocation performed by newAcc indeed happens in the caller's stack frame.
From the perspective of Low * , newAcc is a function in a separate module, and type abstraction is preserved. et al. 2017] ; then λow * , a formal core of Low * after all erasure of ghost code and specifications; then C * , an intermediate language that switches the calling convention closer to C; and finally to Clight. In the end, our theorems establish that: (a) the safety and functional correctness properties verified at the F * level carry on to the generated Clight code (via semantics preservation), and (b) Low * programs that use the secrets parametrically enjoy the trace equivalence property, at least until the Clight level, thereby providing protection against side-channels. Prelude: Internal transformations in emf ⋆. We begin by briefly describing a few internal transformations on emf ⋆ , focusing in the rest of this section on the pipeline from λow * to Clight-the formal details are in the appendix.
λow * : A Formal Core of Low * Post-Erasure The meat of our formalization of Low * begins with λow * , a first-order, stateful language, whose state is structured as a stack of memory regions. It has a simple calling convention using a traditional, substitutive β-reduction rule. Its small-step operational semantics is instrumented to produce traces that record branching and the accessed memory addresses. As such, our traces account for side-channel vulnerabilities in programs based on the program counter model  [Molnar et al. 2006 ] augmented to track potential leaks through cache behavior  [Barthe et al. 2014 ]. We define a simple type system for λow * and prove that programs well-typed with respect to some values at an abstract type produce traces independent of those values, e. g. , our bigint library when translated to λow * is well-typed with respect to an abstract type of limbs and leaks no information about them via their traces.
2 C * : An Intermediate Language We move from λow * to Clight in two steps. The C * intermediate language retains λow * 's explicit scoping structure, but switches the calling convention to maintain an explicit call-stack of continuations (separate from the stack memory regions). C * also switches to a more C-like syntax, separates side effect-free expressions from effectful statements. P ∶∶= ⇀ fun f (x ∶ τ ) ∶ τ { ⇀ s } ê ∶∶= n ⋃︀ () ⋃︀ x ⋃︀ ê + ê ⋃︀ { ⇀ f = ê} ⋃︀ ê. f ⋃︀ & ê → f s ∶∶= τ x = ê ⋃︀ τ x = f ( ê) ⋃︀ if ê then ⇀ s else ⇀ s ⋃︀ return ê ⋃︀ { ⇀ s } ⋃︀ τ x(︀n⌋︀ ⋃︀ τ x = * (︀ ê⌋︀ ⋃︀ * (︀ ê⌋︀ = ê ⋃︀ memset ê n ê The syntax is unsurprising, with two notable exceptions. First, despite the closeness to C syntax, contrary to C and similarly to λow * , block scopes are not required for branches of a conditional statement, so that any local variable or local array declared in a conditional branch, if not enclosed by a further block, is still live after the conditional statement.
2 (λow * to C * ). Let P be a λow * program and e be a λow * entry point expression, and assume that they compile: ⇊ (P) = P for some C * program P and ↓ (e) = ⇀ s ; ê for some C * list of statements ⇀ s and expression ê. Let V be a mapping of local variables containing the initial values of secrets. Then, the C * program P terminates with trace ℓ and return value v, i. e. , P ⊢ ((︀⌋︀,V , ⇀ s ; return ê) In particular, if the source λow * program is safe, then so is the target C * program. It also follows that the trace equality security property is preserved from λow * to C *. We prove this theorem by bisimulation. In fact, it is enough to prove that any λow * behavior is a C * behavior, and flip the diagram since C * is deterministic. That C * semantics use big-step semantics for C * expressions complicates the bisimulation proof a bit because λow * and C * steps may go out-of-sync at times.
From C * to CompCert Clight and Beyond CompCert Clight is a deterministic (up to system I/O) subset of C with no side effects in expressions, and actual byte-level representation of values. Clight has a realistic formal semantics  [Blazy and Leroy 2009; Leroy 2016 ] and tractable enough to carry out the correctness proofs of our transformations from λow * to C. More importantly, Clight is the source language of the CompCert compiler backend, which we can thus leverage to preserve at least safety and functional correctness properties of Low * programs down to assembly. 3 ecall that we need to produce an event in the trace whenever a memory location is read or written, and whenever a conditional branch is taken, to account for memory accesses and statements in the semantics of the generated Clight code for the purpose of our noninterference security guarantees.
CompCert 2. 7. 1 does support such hoisting but as an unproven elaboration step. While existing formal proofs  (e. g. , Dockins' [Dockins 2012, §9. 3] ) only prove functional correctness, we also prove preservation of security guarantees, as shown below. Proof techniques. Contrary to the λow * -to-C * transformation, our subsequent passes modify the memory layout leading to differences in traces between C * to Clight, due to pointer values. Thus, we need to address security preservation separately from functional correctness. For each pass changing the memory layout, we split it into three passes. First, we reinterpret the program by replacing each pointer value in event traces with the function name and recursion depth of its function call, the name of the corresponding local variable, and the array index and structure field name within this local variable.
An alternative is to write bindings by hand, which allows for better performance and control over how data is transformed at the boundary, but requires writing and recompiling potentially error-prone C code. This is the historical way of writing bindings for many languages, including OCaml. We plan to have KreMLin generate these bindings automatically. We used this approach in miTLS, effectively making it a mixed C/OCaml project. We intend to eventually lower all of miTLS into Low *. In this section, we describe two examples (summarized in Table  1 ) that show how Low * can be used to build applications that balance complex verification goals with high performance. First, we describe HACL * , an efficient library of cryptographic primitives that are verified to be memory safe, side-channel resistant, and, where there exists a simple mathematical specification, functionally correct.
A Verified NaCl Library. We implement the NaCl API, including all its component algorithms, in a Low * library called HACL * , mechanically verifying that all our code is memory safe, functionally correct, and side-channel resistant. The C code generated from HACL * is ABI-compatible and can be used as a drop-in replacement for Sodium or TweetNaCl in any application, in C or any other language, that relies on these libraries. Our code is written and optimized for 64-bit platforms; on 32-bit machines, we rely on a stub library for performing 64x64-bit multiplications and other 128-bit operations. We implement and verify four cryptographic primitives: ChaCha20, Salsa20, Poly1305, and Curve25519, and then use them to build three cryptographic constructions: AEAD, secretbox and box. For all our primitives, we prove that our stateful optimized code matches a high-level functional specification written in F *.
We observe that for ChaCha20, Salsa20, and Poly1305, HACL * achieves comparable performance to the optimized C code in OpenSSL and Sodium and significantly better performance than Tweet-NaCl's concise C implementation. Assembly implementations of these primitives are about 3-4 times faster; they typically rely on CPU-specific vector instructions and careful hand-optimizations. Our Curve25519 implementation is about the same speed as Sodium's 64-bit C implementation (donna_c64) and an order of magnitude faster than TweetNaCl's 32-bit code. It is also significantly faster than OpenSSL because even 64-bit OpenSSL uses a Curve25519 implementation that was optimized for 32-bit integers, whereas the implementations in Sodium and HACL * take advantage of the 64x64-bit multiplier available on Intel's 64-bit platforms.
The previous F * implementation of Curve25519  [Zinzindohoué et al. 2016 ] running in OCaml was not optimized for performance; it is more than 100x slower than HACL *. The fastest assembly code for Curve25519 on eBACS is the one verified in  [Chen et al. 2014 ]. This implementation is only 1. 08x faster than our C code, at least on the platform on which we tested, which supported vector instructions up to 256 bits. We anticipate that the assembly code may be significantly faster on platforms that support larger 512-bit vector instructions. AEAD and secretbox essentially amount to a ChaCha20/Salsa20 cipher sequentially followed by Poly1305, and their performance reflects the sum of the two primitives. Box uses Curve25519 to compute a symmetric key, which it then uses to encrypt a 16KB input.
Here, the cost of symmetric encryption dominates over Curve25519. In summary, our measurements show that HACL * is as fast as (or faster than) state-of-theart C crypto libraries and within a small factor of hand-optimized assembly code. This finding is not entirely unexpected, since we wrote our Low * code by effectively porting the fastest C implementations to F * , and any algorithmic optimization that is implemented in C can, in principle, be written (and verified) in Low *. What is perhaps surprising is that we get good performance even though our Low * code, and consequently the generated C, heavily relies on functional programming patterns such as tail-recursion, and even though we try to write generic compact code wherever possible, rather than trying to mimic the verbose inlined style of assembly code.
It also protects file metadata, including the file name and modification time, and it hides the file size by padding the file before encryption to a user-defined size. We verify that our code is memory-safe, side-channel resistant, and that it uses the I/O libraries correctly (e. g. , it only reads or writes a file or a socket between calling open and close). PneuTube's performance is determined by a combination of the crypto library, disk access (to read and write the file at each end) and network I/O. Its aynchronous design is particularly rewarding on high-latency network connections, but even when transferring a 1GB file from one TCP port to another on the same machine, PneuTube takes just 6s. In comparison, SCP (using SSH with ChaCha20-Poly1305) takes 8 seconds.
Cryptographically Secure AEAD for miTLS We use our cryptographically secure AEAD library ( §2. 4) within miTLS  [Bhargavan et al. 2013 ], an existing implementation of TLS in F *. In a previous verification effort, AEAD encryption was idealized as a cryptographic assumption (concretely realized using bindings to OpenSSL) to show that miTLS implements a secure authenticated channel. However, given vulnerabilities such as CVE-2016-7054, this AEAD idealization is a leap of faith that can undermine security when the real implementation diverges from its ideal behavior. We integrated our verified AEAD construction within miTLS at two levels  [Bhargavan et al. 2017]. First, we replace the previous AEAD idealization with a module that implements a similar ideal interface but translates the state and buffers to Low * representations.
This shallow embedding has significant advantages in terms of reducing verification effort and thus scaling up verification to larger programs. This also allows us to port to C only the parts of an F * program that are a performance bottleneck, and still be able to verify the complete program. Verifying the correctness of low-level cryptographic code is receiving increasing attention  [Appel 2015; Beringer et al. 2015; Dodds 2016]. The verified cryptographic applications we have written in Low * and use for evaluation in this paper are an order of magnitude larger than most previous work. Moreover, for AEAD we target not only functional correctness, but also cryptographic security. In order to prevent the most devastating low-level attacks, several researchers have advocated dialects of C equipped with type systems for memory safety  [Condit et al.
Verification happens at the generated C level, which has the advantage of taking the code generation machinery out of the TCB, but has the disadvantage of being far away from the original source code. Bedrock  [Chlipala 2013 ] is a generative meta-programming tool for verified low-level programming in Coq. The idea is to start from assembly and build up structured code generators that are associated verification condition generators. The main advantage of this "macro assembly language" view of low-level verification is that no performance is sacrificed while obtaining some amount of abstraction. One disadvantage is that the verified code is not portable. Our companion paper "Implementing and Proving the TLS 1. 3 Record Layer"  [Bhargavan et al. 2017]  is available online. It describes a cryptographic model and proof of security for AEAD using a combination of F * verification and meta-level cryptographic idealization arguments.
CONCLUSION This paper advocates a new methodology for carrying out high-level proofs on low-level code. By embedding a low-level language and memory model within F * , the programmer not only enjoys sophisticated proofs but also gets to write their low-level code in a more modular style, using features functional programmers take for granted, including recursion and type abstraction. Our toolchain, relying on partial evaluation and the latest advances in C compilers, shows that we can write code in a style suitable for verification and enjoy the same performance as hand-written C code. We are currently making progress in three different directions. First, continuing our integration of AEAD within miTLS, we aim to port the miTLS protocol layer to Low * , in order to get an entire verified, TLS library in C.
A refines B iff there exists R so that A refines B by R. In the following text, we treat label read⇑write (b, n) and read⇑write (b, n, (︀⌋︀) as equal, and if we have a λow * value or substitution, we freely use it as a C * one because coercion from λow * value to C * value is straight-forward. Theorem D. 6 (Safety). For all λow * program lp, closed expression le and closing substitution V , if ⇊ lp = p, ↓ le = ss and sys λow * (lp,V (le)) is safe, then sys C * (p,V , ss) is safe. Proof. Appeal to Lemma D. 12, Lemma D. 16 and Lemma D. 15. □ Theorem D. 7 (Bisimulation). For all λow * program lp, closed expression le and closing substitution V , if ⇊ lp = p and ↓ le = ss, then sys C * (p,V , ss) bisimulates sys λow * (lp,V (le)). Proof. Appeal to Corollary D. 13, Lemma D. 16 and Lemma D. 15. □ Definition D.
End of case. Case Structfield: on case (H, LE (︀(b, n, ⇀ f d) ▷ f d ′ ⌋︀) ↝ (H, LE (︀(b, n, ( ⇀ f d; f d ′ ))⌋︀). Pick C ′ to be (S,V , ss). Because (H, LE (︀(b, n, ⇀ f d) ▷ f d ′ ⌋︀) R C ′ with some m, it must be the case that m ≥ 1 and (H, LE (︀(b, n, ( ⇀ f d; f d ′ ))⌋︀) R C ′ with m -1. End of case. Case IfTrue: on case (H, LE (︀if n then le 1 else le 2 ⌋︀) ↝ brT (H, LE (︀le 1 ⌋︀) and n ⇑ = 0. Appealing to Lemma D. 30, we have ss = if e then ss 1 else ss 2 ; ss ′ and ⎜e⨆︁ (p,V ) = n and le i = V (↑ ss i ) (i = 1, 2) and LE = unravel(S,V (↟ (◻; ss ′ ))). Pick C ′ to be (S,V , ss 1 ; ss ′ ). The semantics of a Clight program is given by the return value of its main function called with no arguments. 7 Thus, given a Clight program p, the initial configuration of a CompCert Clight transition from p is ({}, (︀⌋︀, (︀⌋︀, (︀⌋︀, int r = main()), and a configuration is final with return value i if, and only if, it is of the form ({}, _, _V , _, (︀⌋︀) with _V (r ) = i.
Hoisting local variables is not supported in the verified part of CompCert. This example shows the following issue: when producing the trace, the memory blocks corresponding to the accessed memory location will differ between the non-hoisted and the hoisted C * code. Indeed, in the non-hoisted C * code, only one variable x is allocated in the stack, whereas in the hoisted C * code, two variables x 1 and x 2 corresponding to both branches will be allocated anyway, regardless of the fact that only one branch is executed. Thus, in the C * code before hoisting, allocating x will create, say, block 1, whereas after hoisting, two variables will be allocated, x 1 at block 1, and x 2 at block 2. Thus, the statement * (︀x + 0⌋︀ = 1729 in the C * code before hoisting will produce read (1, 0, (︀⌋︀) on the trace, whereas its corresponding translation after hoisting, * (︀x 2 + 0⌋︀ = 1729, will produce read (2, 0, (︀⌋︀).
25. C * 3 Amended Configuration Reduction in C *. 10 Then, both executions apply the same C * 2 rules since C * 2 small-step rules are actually syntax-directed. □ E. 4. 2 Normalized traces. Now, consider an execution of C * 2 from some initial state. In fact, for any block identifier b defined in S, it is easy to prove that it actually corresponds to some variable defined in the scope. The corresponding VarOfBlock algorithm is shown in Figure  24. Then, let C * 3 be the C * 2 language where the Read and Write rules are changed according to Figure  25 , with event traces where the actual pointer is replaced into an abstract pointer obtained using the VarOfBlock algorithm above. Lemma E. 7 (C * 2 to C * 3 functional correctness). If sys(p,V , ss) has no unambiguous variables, then sys(p,V , ss), has the same behaviors in C * 2 with event traces with read, write removed, as in C * 3 with event traces with read, write removed.
As far as I understood, a Low * program obtained from a well-typed F * program should be safe with any memory allocator, including with a memory allocator which never reuses previously allocated block identifiers, as in CompCert. 11 In particular, a Low * program safe with such a CompCert-style allocator will actually never try to access memory through a dangling pointer to a local variable no longer in scope. Then, traces with concrete pointer values are preserved from Low * to C * 2 with the allocator fixed in advance in all of Low * , C * and C * 2; and functional correctness and noninterference are also propagated down to C * 3 using the same memory allocator. There should be a way to prove the following: Lemma E. 11. If a C * 3 program is safe with a CompCert-style memory allocator, then it is safe with any memory allocator and the traces (with abstract pointer representations) are preserved by change of memory allocator.
Proof. Lock-step simulation where the configurations have the same structure but a (functional but not necessarily injective) renaming of block identifiers from a CompCert-style allocator to any allocator is maintained and augmented throughout the execution. In particular, we have to prove that VarOfBlock is stable under such renaming. □ If so, then for the remainder of this paper, we can consider a CompCert-style allocator. Hoisting. Definition E. 12 (Hoisting). For any list of statements ss with unambiguous local variables, the hoisting operation hoist(ss) = (ads, ss ′ ) is so that ads is the list of all array declarations in ss (regardless of their enclosing code blocks) and ss ′ is the list of statements ss with all array declarations replaced with (). Then, hoisting the local variables in the body ss of a function is defined as replacing ss with the code block {ads; ss ′ } where hoist(ss) = (ads, ss ′ ); and then, hoisting the local variables in a program p, hoist(p), is defined as hoisting the local variables in each of its functions.
e. after its corresponding variable has fallen out of scope), since in the latter case, it corresponds to any block identifier and nothing has to be proven then (since accessing memory through it will fail in the source, per the fact that the CompCert-style memory allocator will never reuse b. ) □. This is because, unlike GCC, CompCert cannot detect that a structure is never taken its address, which is mostly the case for local structures in code generated from C *. This is due to the fact that, even at the level of the semantics of C structures in CompCert, a field access is tantamount to reading in memory through a constant offset. In other words, CompCert has no view of C structures other than as memory regions. To solve this issue, we replace local structures with their individual non-compound fields, dubbed as structure erasure.
Then, the transformation back to C * 3 exactly preserves the traces of C * 4 programs, so that we obtain both functional correctness and noninterference at once: Theorem E. 18 (StructRet correctness). If sys(p,V , ss) is safe in C * 4 and has unambiguous local variables, then it has the same behavior and trace as sys(StructRet(p),V , StructRet(ss, )). Proof. Forward downward simulation, where the compilation invariant also involves block identifier renaming from Definition E. 13 due to the new local arrays introduced by the transformed program. Each C * 4 step is actually matched by the same C * 3 step, except for function return and return from block: for the RetBlock rule, the simulation diagram has to stutter as many times as the level of block nesting in the source program before the actual application of a Ret 4 rule.
Fortunately, CompCert introduces the notion of built-in functions, which are special constructs whose semantics can be customized and that are guaranteed to be preserved by compilation down to the assembly. Thus, we can populate the values of local non-stack-allocated variables of a C * entrypoint by uniformly calling builtins in Clight, and only the semantics of those builtins will depend on secrets, so that the actually generated Clight code will be syntactically secret-independent. Translating C * 2 expressions with no structures or structure field projections into CompCert Clight is straightforward, as shown in Figure  33. For any C * 2 expression e of type t, assuming that A is a set of local variables to be considered as local arrays, we define C t A (e) to be the compiled Clight expression corresponding to e.
ACKNOWLEDGMENTS We thank the anonymous reviewers for their excellent reviews. We also thank  Abhishek Anand  and  Mike Hicks , for useful feedback and discussion which helped shape the work presented here, as well as  Armaël Guéneau , for his work on a mechanized proof. J-K. Zinzindohoué  and  K. Bhargavan  received funding from the  European Research Council (ERC)  under the European Union's  Horizon 2020 research and innovation programme  (grant agreement no. 683032 -CIRCUS ). C. Hriţcu was in part supported by the  European Research Council  under  ERC Starting Grant   SECOMP (715753 ).