1 Introduction

The standardization of cryptographic APIs in JavaScript through the W3C Web Cryptography API, WebCrypto [31], has made strong cryptography available to web developers. In theory, this allows non-experts to implement true end-to-end encryption of confidential data. However, mistakes are easily made when developers use cryptographic APIs. For example, the JavaScript snippet in Listing 1 generates secure keys and then encrypts and signs a message before sending it. Here, the developer made the mistake of appending a signature of the plaintext to the message, allowing an observer to identify retransmissions of the same message. Mistakes like this undermine the security of the overall system, even when the implementation of the cryptographic API itself is correct.

Such mistakes are not exclusive to JavaScript, but in fact common across languages [8, 16, 20]. Alas, JavaScript exacerbates the problem, due to its dynamic nature and unconventional semantics [22], which thwart traditional analysis techniques and offer plenty of opportunities to violate API specifications. Existing work on JavaScript focuses on the verification of protocol implementations through restriction to small subsets of the language [2, 14]. There is currently little support to help non-expert developers avoid introducing critical security bugs into applications built on full JavaScript.

figure a

In this work, we introduce a mechanism which rules out misuse of trusted APIs in JavaScript code through runtime enforcement. We extend the concept of Security Annotations [19], type-like tags which represent security properties, such as whether a value is ciphertext or a cryptographic key. Security Annotations are orthogonal to the existing type system and composable to allow for the expression of multiple distinct security properties.

In particular, we make the following contributions:

  • We formalize a runtime semantics for Security Annotations in JavaScript by extending an existing formal semantics for a core of JavaScript, S5 [22] (Sect. 4).

  • We mechanize Security Annotations, building upon an existing implementation of S5. We extend this to a reference interpreter for JavaScript programs through extending the JavaScript-to-S5 desugaring relation (Sect. 5).

  • We provide an annotated fragment of the WebCrypto API which defines safe usage of the API through Security Annotations. Developers can replace the WebCrypto API with this annotated copy, which allows our mechanism to report violations of the otherwise implicit API specifications. We demonstrate how this approach can be used to avoid common cryptographic pitfalls by detecting violations of security properties in a case study (Sect. 5.3).

  • We provide safety guarantees for this Security Annotation mechanism, and extend these to describe resulting security guarantees for programs using the annotated WebCrypto fragment (Sect. 6).

2 Background

We begin by introducing necessary background on Security Annotations (Sect. 2.1) and our underlying JavaScript semantics (Sect. 2.2).

2.1 Security Annotations

Security Annotations represent security properties valid on objects or values within a program [19]. For example, the return value of a trusted key generation API is a valid cryptographic key, so could carry an annotation  . Annotations are composable: if the value has also been generated as a cryptographically secure random value (CSRV), then it can be annotated through composition  , via the commutative operator \(*\). Security properties are hierarchical: for example,  is more specific than  . Security Annotations therefore have a notion of subannotation judgments, e.g.,  . Combined with the composition operator, this yields a lattice of security annotations. We include the rules defining this lattice in Fig. 1. These judgments follow those given in Mitchell et al. [19]; additional rules governing reflexivity, transitivity and permutations are included for completeness. In these rules, \(S_i\) are arbitrary Security Annotations and  is the least specific Security Annotation, representing a lack of security properties.

Fig. 1.
figure 1

Hierarchical Security Annotation judgments [19].

Full size image

Mitchell et al. [19] enforce Security Annotations statically within a small lambda calculus. The expression adds S as an annotation to v, representing newly valid security properties. Similarly, discards S from v, using a  operator to remove an annotation whilst ensuring super-properties remain valid. We cut the annotation \(S_2\) from \(S_1\) via the following definition: is the annotation R with (i) \(S_1 \prec :R\) and (ii) \(R \nprec :S_2\) such that whenever \(R'\) also satisfies (i) and (ii) in place of R, then \(R \prec :R'\) and \(R' \nprec :R\) [19].

2.2 S5: A Semantics for JavaScript

S5 [22] is a lambda calculus-like language which reflects the semantics of the strict mode of EcmaScript 5.1 (ES5). S5 is accompanied by a desugaring function, which takes native JavaScript source programs and translates them to S5 programs. S5 itself is described via small-step semantics, incorporating ES5 features such as getters, setters and eval. The language is not a complete reference implementation for the entire standard but is tested against the official ES5 test suite.

Terms in S5 are 3-tuples comprised of an expression, e, a store \(\sigma \) (mapping locations to values) and an object store \(\varTheta \) (mapping references to object literals); the evaluation context is denoted E. The reduction relation \(\rightarrow \) is split into four parts dependent on which portions of the term are manipulated; their definitions are given in Fig. 2. For ease of reference, S5’s syntax is given in Appendix A; full details of S5 are contained in the work of Politz et al. [22].

Fig. 2.
figure 2

The reduction relations for S5 [22].

Full size image

3 Overview

We present an overview of our approach. First, we discuss how Security Annotations express properties of cryptography APIs (Sect. 3.1). We describe, through example, how such properties are enforced without changes to client code (Sect. 3.2).

3.1 Annotating APIs with Security Annotations

We provide a thin layer of JavaScript code (a shim) which adds pre- and postconditions to WebCrypto APIs. Listing 2 gives an example of such a shim for the  API, which encodes the runtime specification for the API. This shim is included directly into application code via  ; line 15 redefines WebCrypto’s  . This is the only addition an application developer need make to their codebase; the propagation of these annotations is governed by the mechanisms formalized in Sect. 4. Security Annotations on arguments are checked against the API’s preconditions, made explicit through annotation guards. Security Annotations are then attached to return values of functions when these API calls contain specific postconditions.

Lines 1–3 define the annotation lattice for this API; this implicitly contains  , which represents a lack of security properties. The syntax defines orthogonal annotations \(S_1, \ldots , S_n\). Lines 2–3 use the syntax , to define new annotations \(S_1, \ldots , S_n\) with \(S_i \prec :S\) for each i.

figure r

Security Annotations are enforced at function boundaries via , which ensures meets the annotation guard S. For example, on line 8, we enforce that if the symmetric encryption algorithm AES is selected, then the  argument to the function is annotated with  . On line 6, checks that the specified object property meets its guard. In this case, we check that the initialization vector supplied as part of the  object is a properly generated random value.

Postconditions are attached as annotations to return values. Encryption is performed by the original API (line 12); annotations representing newly valid security properties are then attached (line 13). First,  attaches all annotations from the  argument to  : security properties of the data are not invalidated as a result of encryption. The advantage of  is that we do not need to know the precise annotations of  . The exception is that if  was annotated with  (e.g., if it had been previously decrypted), we discard this annotation via the  operator. Finally, we attach  to the return value via the  operator.

3.2 Transparent Property Enforcement

The application in Listing 1 sends an encrypted, signed message across a network via the  method (line 15). The application developer uses WebCrypto in order to encrypt and sign this message; without our drop-in WebCrypto shim this application will execute and the developer will be unaware of a security flaw. Although individual wrapper functions for signing and encryption are correct, there is a logical error that causes a security bug. In particular, a signature is generated of the plaintext and sent alongside the corresponding ciphertext. This undermines the security of the application: attacks against this signature can reveal details about the underlying plaintext.

At runtime, the application builds the object to send: the  property is constructed by calling the developer’s  function. This function is correct: the array stored in  is annotated with  , the postcondition of WebCrypto’s  . The  API, when the algorithm is symmetric (i.e., in the case of both HMAC and AES), returns a valid symmetric key (annotated with  ). The call to WebCrypto’s  succeeds since each argument satisfies the specification (Listing 2). Next, the developer calls  with argument the unencrypted  . Similarly, the key is correctly generated via the API. However, there is an implicit precondition of  —data to be signed must be ciphertext to avoid common attacks against the signature revealing information about it. By using our drop-in shim for WebCrypto, this bug is detected: since  is not annotated with  an error is thrown on entry to  , reporting the violation to the developer.

Fig. 3.
figure 3

Syntax modifications to add Security Annotations to S5.

Full size image

4 Security Annotations for S5

We formalize Security Annotations within S5 [22], starting with modifications to the syntax (Sect. 4.1). We describe mechanisms for manipulating annotations (Sect. 4.2), runtime enforcement (Sect. 4.3), and their effect on the rest of S5 (Sect. 4.4).

4.1 Syntax

The additions and modifications to the syntax of S5 (given in Appendix A) to incorporate Security Annotations are contained in Fig. 3. We introduce atomic annotations a, which represent a single security property, and general annotations S, which are either  , the least specific annotation, an atomic annotation, or the composition of two annotations, given by \(*\). Annotations are only attached to certain prevalues w. Prevalues which should not be annotated are given by \(w'\), values are then either references r,  or \(w'\), where is syntactic sugar for the pair of an annotatable value w along with its corresponding Security Annotation S. An additional modification to the syntax reflects the addition of annotations to objects: we consider pre-objects, \(\theta '\), which form objects when annotated with a Security Annotation S. We annotate objects directly as opposed to their references; properties within objects are annotated in the same manner as values. When an object is modified, previously valid security properties on the object are no longer guaranteed: modifying an object field should alter the annotations associated to the field, and also the annotations of the overall object.

Additional expressions, e, based on manipulating security annotations, cover the  ,  and  constructs. We add evaluation contexts, \(E'\), to cover these cases, where these are built in the same manner as in S5 (see Appendix A). Finally, enforcement of Security Annotations is added to functions via the form ; this does not require modification of the evaluation contexts.

4.2 Coercing Security Annotations

The evaluation judgments for coercion of annotations on values and objects are given in Fig. 4, distinguished by case analysis on values. The expression  upcasts v to a more specific annotation, achieved by composing the previously valid annotation with S. Dependent on whether we treat (in [E-AsW]), or a reference r ([E-AsR]), we make use of distinct reduction relations (Fig. 2). In the former case, [E-Compat] is used to govern the evaluation. In the latter, [E-Objects] is used to modify the object’s annotation in the object store. Finally, we throw an error whenever a function,  or  is passed to one of these expressions treating coercion of annotations (e.g., [E-AsW’]). The case analysis for  are similar; downcasts v to a less specific annotation. This is accomplished via the  operator (Sect. 2.1) to prune the S from the annotation of v. Listing 2 illustrates the use of  to ensure properties of data are still valid after encryption by copying annotations from one value (or object) to another. As with  , the addition of newly valid annotations does not render previous annotations invalid, so composition unifies them; the evaluation rules are therefore similar in structure.

Fig. 4.
figure 4

Judgments for coercing annotations:  ,  and  .

Full size image

4.3 Checking Security Annotations

Figure 5 codifies the enforcement of Security Annotations at function boundaries. [E-App] governs the case when arguments meet their annotation-guards and the function is evaluated. This rule inspects the object store (to look up object annotations when arguments are references) and modifies the variable store (to bind arguments to the corresponding variables); we therefore use the standard reduction relation rather than the split components (Fig. 2). To reflect the hierarchy of the annotation lattice, this rule bakes in subsumption, e.g., enforcement of  would accept the more specific  . A common JavaScript paradigm is for non-annotatable values, e.g., functions, to be passed as arguments; we insist the guard for such arguments is  , i.e., no security precondition. For any annotatable values, , we insist S satisfies the guard \(S'\). For references r, we look up the corresponding object and insist the annotation meets the guard. Direct checking of object properties and the  argument is achieved via source-to-source rewritings, described in Sect. 5.2. [E-AppFail] describes what happens when annotation-checking fails, i.e., whenever an argument carries a less precise annotation than its guard.  is thrown to report the potential security vulnerability to the user, rather than simply halting evaluation.

Fig. 5.
figure 5

Function application with Security Annotation enforcement.

Full size image

4.4 Completing S5 with Security Annotations

The rest of S5 remains largely unchanged. After object fields are manipulated, there is no guarantee the object annotation remains valid. For example, modifying the  field of a key object returned from the  API may undermine the security of any future operation involving the key. Any previously valid security properties on the object can no longer be guaranteed;  is therefore associated as the object’s annotation. Figure 6 includes judgments for field manipulation, including adding fields which do not exist and writable ‘shadow’ fields. These semantics are transparent to annotations to allow prevalues to govern control flow, e.g., the  property must be  in [E-DeleteField].

Fig. 6.
figure 6

Judgments for setting, deleting and adding fields.

Full size image

5 Security Annotations for JavaScript

We describe the mechanization of this model (Sect. 5.1) and a desugaring relation which allows the execution of JavaScript with Security AnnotationsFootnote 1. We discuss the annotation checking of object internals (Sect. 5.2) and demonstrate its operation on a case study (Sect. 5.3).

5.1 Implementing Security Annotations in S5

We mechanize Security Annotations on top of the existing reference implementation of S5 [22]. Alongside object and variable stores, we maintain a third annotation store, the lattice of valid annotations in the program. Security Annotations are declared via the  and  expressions described in Sect. 3.1. These expressions modify the annotation store to reflect additions to the lattice and evaluate to  . Using an annotation prior to declaration results in an exception. The lattice is also inspected in function application (Fig. 5) to compare annotations with respect to subsumption. Section 4 describes functions in which each argument is checked against some annotation guard. In implementation, we retain enforcement-free functions and do not insist every argument has an annotation-guard. This allows reuse of existing ES5 environment implementations described in the work of Politz et al. [22].

5.2 A Reference Interpreter for Security Annotations in JavaScript

We execute JavaScript code with Security Annotations by extending the JavaScript-to-S5 desugaring relation. We extend the syntax of JavaScript by adding Security Annotations and function guards, as well as the expressions ,  ,  ,  and  . Our desugaring rewrites these expressions into their S5 equivalents, which are then executed in the reference interpreter.

Checking Object Properties. Listing 2 demonstrates the need for checking properties of objects. We achieve this via source-to-source rewritings at the JavaScript level; these are simplified by an assert function

figure cj

There are three possible cases; first,  checks  meets S. We check the specified property exists, and insist it satisfies the guard S:

figure cm

Second, checks all properties meet the guard S; to achieve this we iterate over all object properties:

figure co

Finally, checks at least N properties satisfy S. As before, we iterate over object properties, counting the number that meet the guard:

figure cq

Checking  . Functions have an implicit  argument, the context object in which the current code is executing. In the manner of checking object properties, we check this via the syntax which is rewritten to .

5.3 Using the Reference Interpreter

We provide a reference implementation of Security Annotations for the correctness of future implementations in native JavaScript. Our interpreter translates a subset of Node.js programs into S5 programs; we demonstrate the scope of this reference interpreter by describing the modifications to programs necessary for execution. We outline how we envisage Security Annotations being used by developers to detect security vulnerabilities through case study within our interpreter.

A Client-Server Application. We implement a small chat application which takes as argument a confidential message a client wishes to transmit to a serverFootnote 2. The server and client negotiate a key exchange, and an encrypted copy of this message is sent to the server, which decrypts it. We omit authentication from this case study for simplicity of presentation. WebCrypto is not implemented in Node.js, so we construct a synchronous mock using the Node.js  module.

Execution in S5. Library mocks are necessary to execute the case study in S5. S5 does not support asynchronous code, so we construct a synchronous mock of the networking API,  . An extension to asynchronous code is possible in principle based on an existing formalization of JavaScript promises [18]. Second, cryptographic operations are mocked as stub functions returning objects of the same underlying structure. Finally, S5 programs do not take input, so we declare  to simulate this.

Completing the WebCrypto Shim. Listing 3 contains an annotated shim of a fragment of WebCrypto for use by developers. These method specifications follow the same structure as Listing 2.  fills the supplied array with random values, so this array is annotated with  . Despite the lack of a return, the annotation on this array persists because the annotation is attached directly to the object.  constructs a key (or key pair) object for the supplied algorithm; postconditions of this method are differentiated by case analysis.  is used to compute a shared secret key from the other party’s public key and the private key. The contract for  is similar to  ; we do not enforce  against  —or that the IV is randomly generated—to allow decryption of messages received across a network.  allows public keys received across a network to be formatted for use with other WebCrypto APIs. This API allows the upcasting of arbitrary data; however, without  , it would be impossible to use WebCrypto across a network.

A Security Property Violation. When constructing the IV, the developer ensures that it can be encoded directly as an ASCII string. Despite correctly generating an IV of the same size as the cipher block size (calling  on a  of size 16), they reduce entropy of the IV by zeroing the top bit of each element of this array. This causes the IV to contain only 112 bits of entropy, less than the block size: a potential security flaw which does not visibly affect runtime behavior. To detect such bugs, a developer includes our WebCrypto shim. The IV is initially generated by a WebCrypto API call and annotated with  ; however, the manipulation of the array drops the annotation (per [E-SetField] in Fig. 6). Since the  property of the  object is not annotated with  , the call to  fails,  is thrown and this security flaw is reported to the developer. When the loss of entropy is removed, no error is thrown; the security pre- and postconditions enforced in the shim are respected.

6 Properties of Security Annotations

We discuss safety guarantees for S5 programs with Security Annotations (Sect. 6.1) and extend this to security guarantees (Sect. 6.2). Finally, we apply this to prove security of our case study (Sect. 6.3). Throughout this section, we assume all programs discussed terminate.

6.1 Safety Guarantees

We adopt a relatively modest notion of safety: first, a program is safe if it does not evaluate to an exception as a result of a function argument failing to meet the annotation guard. Second, the program should not coerce the annotation of a non-annotatable value, e.g.,  . This gives us the definition:

figure dr

Definition 1

(Annotation Safety). An S5 program is safe with respect to Security Annotations (or, annotation safe) if the execution of the program does not result in either a  or  exception.

Although programs in S5 are deterministic, programs in JavaScript (or any meaningful language) are not: their execution depends on the DOM or user input. Suppose \(\mathcal {P}\) is a program expecting input, we extend Definition 1 as follows:

Definition 2

(Annotation Safety for Programs with Input). \(\mathcal {P}\), is annotation safe if no execution of the program results in either a  or  exception.

Consider a family of S5 programs, \(\varPi \), which are deterministic and simulate input by declaring a global variable  assigned to an object containing N fields. For each field, \(f_i\) suppose there is an accompanying value \(v_i\). For each \(v_i\), we fix a base type and range over all possible prevalues (and  , which simulates a lack of input). If \(v_i\) is a reference to an object, we range over all possible objects \(\theta \). The resulting family of programs represents the space of possible executions for \(\mathcal {P}\). We can therefore reformulate Definition 2:

Lemma 3

Let \(\mathcal {P}\) be an S5 program with input and \(\varPi \) the family of deterministic programs p describing all possible inputs for \(\mathcal {P}\). Then \(\mathcal {P}\) is annotation safe if and only if every program \(p \in \varPi \) is annotation safe.

Proof

By construction, each execution of \(\mathcal {P}\) is considered as a separate deterministic program P so the result is immediate. \(\square \)

Since this family \(\varPi \) is very large, we formalize safety in terms of a subset of these programs. Let \(\pi \) be the set of all \(p \in \varPi \) following exactly the same sequence of evaluation judgments. This set of S5 programs corresponds to a single control-flow path of \(\mathcal {P}\): so if any p is annotation safe, so are all programs in \(\pi \). Since the union of all (clearly disjoint) possible paths \(\pi \) is equal to the overall family of programs \(\varPi \), we can obtain a simpler notion of safety for \(\mathcal {P}\):

Theorem 4

Let \(\varPi \) be the family of deterministic programs describing all possible inputs for \(\mathcal {P}\). Consider all disjoint subsets \(\pi \subseteq \varPi \) representing single control flow paths of \(\mathcal {P}\), and for each, choose a single \(p \in \pi \). Then \(\mathcal {P}\) is annotation safe if and only if each p is annotation safe.

Proof

Suppose first that \(\mathcal {P}\) is annotation safe. Then by Lemma 3, we know every \(P \in \varPi \) is annotation safe. Since each \(\pi \subseteq \varPi \), each p must be annotation safe as required. For the other direction, suppose each p is annotation safe. Pick one such p, and the subset of \(\varPi \) to which it belongs, \(\pi \). Let \(p'\) be some other program in \(\pi \), and suppose that \(p'\) is not annotation safe. Then the execution of \(p'\) results in either a  or  exception. This means that the final evaluation judgment applied in the evaluation of \(p'\) is either [E-AppFail], [E-AsW’], [E-DropW’], [E-CpW’V] or [E-CpVW’]. Since p and \(p'\) both belong to \(\pi \), they follow the same sequence of evaluation judgments. But then p is not annotation safe, which is a contradiction. Thus each p in \(\pi \) is annotation safe, and extending this across all disjoint subsets \(\pi \) of \(\varPi \), each program in \(\varPi \) must be annotation safe. Applying Lemma 3 again, we are done. \(\square \)

This result says that if any set \(\pi \) is not safe, then some control-flow path in \(\mathcal {P}\) violates the Security Annotation specification of the program, indicating a possible security vulnerability. This description of safety requires us to find these subsets \(\pi \) to obtain a guarantee. In practice, this is equivalent to enumerating all control flow paths of a program over all types of input values and objects, which makes our mechanism ideally suited for combination with feedback-directed fuzzing or dynamic symbolic execution [17].

6.2 Security Guarantees

Let L be a library and \(L'\) an annotated shim of this library; any security guarantees are conditional on the correctness of L, e.g., that WebCrypto itself is a correct implementation of cryptographic primitives. Let P be an S5 program which calls L, and suppose the developer of P in-lines this annotated shim in a program \(P'=L';P\). We assume that P does not contain any expressions which manipulate Security Annotations. We can make the following (overapproximate) claim, which states that the whenever \(P'\) is annotation safe, it respects the security properties enforced by the Security Annotation specifications of the methods in \(L'\).

Lemma 5

Suppose \(P'\) is annotation safe. Then the Security Annotation specifications described in \(L'\) are respected.

Proof

Suppose a Security Annotation specification in \(L'\) is not respected. Then some function precondition fails, so the judgment [E-AppFail] is evaluated, contradicting our assumption that \(P'\) is annotation safe. Since P does not involve the manipulation of Security Annotations, any annotations must be the postconditions of an API call in \(L'\); hence these specifications are respected. \(\square \)

Analogously to Sect. 6.1, we extend this result to programs with input:

Theorem 6

Let \(\mathcal {P}\) be a program with input and suppose \(\mathcal {P}' = L'; \mathcal {P}\) is annotation safe. Then the Security Annotation specifications described in \(L'\) are respected.

Proof

This is immediate from the combination of Theorem 4 and Lemma 5. \(\square \)

6.3 Security Guarantees in Practice

We use Theorem 6 to describe concrete security guarantees for the case study outlined in Sect. 5.3, which are conditional on the correctness of WebCrypto. Recall that after fixing the security vulnerability involving the ASCII-encoded IV, when a message supplied as argument, the program executes without error; if no message is provided the application simply reports this to the user and exits. Both control-flow paths of this program are annotation safe. Referring to the specifications described in our WebCrypto shim (Listing 3), there are two caveats to our claim; the first assumes the developer does not leak keying material and the second relates to the omission of authentication from the case study.

Theorem 7

Suppose that: (i) neither the symmetric key nor either party’s secret keys are leaked across the network, and (ii), an attacker impersonates neither party. Then encrypted messages sent by the client can only be read by the server.

Proof

The application does not manipulate annotations; when executed with a non-annotated copy of the library the program is annotation safe. As described above, both control-flow paths of the program are annotation safe with our annotated library in-lined, we can directly apply Theorem 6. It remains to demonstrate the specification enforced by the annotation library. The encryption—via AES-CBC with a 128-bit key—is secure only when the symmetric key has been securely derived, and the IV is a block-sized CSRV (Listing 2). Our WebCrypto specification enforces the CSRV portion of the contract directly: calling  annotates the IV with  (lines 7–9 of Listing 3), and this array is not subsequently modified, the annotation check on entry to  passes.

Second, the symmetric key used for AES must be shared between the two parties secretly. The key is derived through an ECDH key exchange; both the server and client use  (lines 11–20 of Listing 3) to compute a key pair. Public keys are exchanged, and validated it through  (lines 36–39). The client supplies their private key and the server’s public key to  (lines 21–26). Neither key has been tampered with, so the client’s key is annotated with  and the server’s with  . This satisfies the guard of  , and so the key for AES is computed, and annotated  . The provenance of the secret key as derived from safe API calls can be confirmed, so the guard against the key in  succeeds (line 10 of Listing 2). Therefore, only someone in possession of the private key corresponding to the server’s public key can read the message supplied as  to this API. \(\square \)

7 Related Work

Checking Cryptographic API Usage. Mitchell et al. [19] introduce Security Annotations within a lambda calculus (discussed in Sect. 2.1); this paper extends this work to JavaScript. Recent work on cryptographic API use in Android applications shows that the majority of cryptographic bugs are due to misuse of APIs [16]; Egele et al. [8] show that such errors are common. Nadi et al. [20] survey usage of Java cryptographic APIs, and argue that the APIs are too low-level and require implicit understanding of the underlying cryptographic protocols. Krüger et al. [15] present CrySL, a domain specific language for the specification of correct usage of cryptographic APIs, focusing on the Java Cryptography Architecture. Our approach of encoding pre- and postconditions via security annotations on values and objects embraces the dynamicity of JavaScript which is notoriously difficult to statically analyze.

JavaScript Analysis. While our approach is purely dynamic, various dialects allow for the static checking of JavaScript code [6, 7, 23, 30]. The effective use of such static typing approaches would require modification of APIs and semantics, e.g., prohibiting byte array indexing of Key types. Design-by-contract systems for JavaScript [13] enforce program properties directly expressible within the language. Our work focuses on security properties which cannot be directly expressed in this manner. Previous work on cryptographic testing for JavaScript focuses on implementations of the underlying cryptographic protocols. This work runs parallel to our own: we assume the correctness of these implementations and check existing usage of these APIs. Taly et al. [29] describe an automatic analysis to ensure security-critical APIs correctly protect resources from untrusted code. Domain-specific languages [2, 3, 14] have been proposed to enable verification of bespoke implementations by cryptographic experts. Existing programs are not amenable to this approach, since these languages are small subsets of JavaScript without many of the common idioms and advantages of the language.

Type-Based Approaches for Security. Type systems for F#, such as F7 [1, 4, 5] and F* [28], allow for the description of security properties of terms via dependent types which are checked statically. Static security type systems [24] to enforce secure information flow offer strong guarantees but have proved impractical in the JavaScript setting. Work on JavaScript monitors for information flow [10, 26] provide mechanisms for dynamic enforcement of this in JavaScript; work on information flow monitoring in the presence of libraries [11] extends the applicability of monitor-based approaches. We follow a similar dynamic tag-based approach as such approaches [10], however we adopt a fine-grained system allowing for declassification coupled with precondition checking through annotation guards on functions. COWL [12, 27] is an information flow control system for web browsers preventing third-party library code from leaking sensitive information, achieved via the labeling of browser contexts.

Formalizing JavaScript. Various formalizations of JavaScript exist [9, 21, 22, 25]. \(\lambda _\text {JS}\) [9] and its successor S5 [22] provide a small language modeling the key features of JavaScript and have been extended to provide models for static and dynamic analyses. S5 remains close to the minimal lambda calculus described by Mitchell et al. [19], which allowed for a natural translation of Security Annotations.

8 Conclusions and Future Work

In this paper we described a formal model for Security Annotations in JavaScript, a mechanism to help non-expert developers avoid introducing security-critical bugs. We introduced a runtime semantics for Security Annotations in a core of JavaScript and presented a reference implementation of this system. We specified a partial fragment of the WebCrypto API in terms of Security Annotations, and demonstrated how to use it to detect a potential security vulnerability. Finally, we described the security guarantees offered by Security Annotations.

In future work, we plan to further develop Security Annotations as a runtime analysis for JavaScript by implementing them as an extension for the full language via source code instrumentation. The semantics described in this paper and accompanying implementation serve as a reference to guide the correctness of Security Annotations in full JavaScript.

Fig. 7.
figure 7

The syntax of S5 [22].

Full size image