Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The World Wide Web Consortium (W3C) has commenced work on the Web Cryptography API [3], which defines cryptographic primitives to be deployed across browsers and native Javascript environments. This process has begun in the W3C Web Cryptography Working Group, driven by all major browsers and also open to the wider community.Footnote 1 Started in 2012, the W3C Web Cryptography Working Group is finalizing the standard for completion by the end of 2015, with the design being led by Ryan Sleevi of Google with Mark Watson of Netflix as co-editor. The API is already implemented across Chrome 37 and above (including Android), Mozilla version 36 and above, Opera 27 and above, Safari 8 and above, and Internet Explorer 11 and Microsoft Edge. Thus, the W3C Web Cryptography API is the primary Web-facing cryptography API for the foreseeable future.

Like any API, the Web Cryptography API (informally called the “WebCrypto API”) needs an impartial and thorough analysis to determine its security properties. Cryptographic APIs, and even cryptographic libraries such as OpenSSL, that have not received such an analysis until after widespread deployment have resulted in dangerous security incidents in validating TLS certificates [20]. Given that the W3C’s mission including security reviews, the W3C explicitly worked with the larger community discover possible security vulnerabilities and formally prove the guarantees that the Web Cryptography API could provide. Due to an unfortunate tendency of Web developers to bring incorrect expectations (brought from other environments) to Javascript and to (incorrectly) believe that the Web Cryptography API ‘magically’ makes the Javascript browser environment a suitable platform for secure Web applications, it is important to be able to state precisely the security properties of the Web Cryptography API and what attacks are inherent in the API design as well as its operation in the Javascript browser environment. In the future, these kinds of attacks need to be mitigated so that the use of the Web Cryptography API matches intuitive developer expectations around the use of security APIs.

Section 2 explains in detail the role of formal modeling. Section 3 overviews existing background on Javascript cryptography, followed by relevant literature describing the formal analysis of APIs and Web applications. In Sect. 4, we describe the formal modeling of the Web Cryptography API using the AVISPA language, and describe the experiments we used to verify various security properties in a number of scenarios, including a successful attack on key-wrapping that can be generalized to attacks on key exchange. The behavior of key wrapping and key usages in the API would seem to violate the expectations of most developers who want to use the API. In Sect. 5 we discuss algorithm selection in the WebCrypto API, pointing out well-known errors in their algorithm selection and error codes, and these problems were accepted and our proposed fixes became part of the current WebCrypto API. In Sect. 6 we summarize what properties future standards need to improve the security properties of the Web Cryptography API in particular and the future application of formal API modeling to new standardized APIs and protocols at the W3C.

2 The Role of Formal Modeling in Standardization

In the process of standardization, there is a desire to offer as much functionality to developers as possible, while simultaneously preventing them from making mistakes. In terms of cryptographic APIs like the WebCrypto API, this can lead to handing the application developers a “kitchen sink” of cryptographic primitives, which inadvertently may give a developer “enough rope to hang themselves.” Unlike protocols, APIs typically do not have precisely stated threat models and security properties. This is a mistake, as security flaws at the API level are automatically inherited by application that deploy the API and the primitives provided by the API.

Although there is a reasonable argument to give developers only “high level” APIs that may include suitable defaults, these APIs by nature must build on “low level” APIs that provide access to a large range of cryptographic primitives even if the “low level” API is not accessible or hidden from the developer. In the Web Cryptography API, it was chosen to release the “low level” WebCrypto API and not explicitly work on a “high level” cryptographic API or provide defaults. While it seems that users will generally use the highest-level of abstraction available to them, the Working Group has decided that given that the field of cryptography is in flux around issues such as elliptic curves and attacks on RSA, it would be unwise to provide any defaults that may become outdated in the standard. Instead, a ‘high-level’ API with appropriate defaults can be created that would build from the primitives in the Web Cryptography API.

The process of standardization in the field of security needs to incorporate formal methodology in order to state the security properties and discover attacks before a standard is released. As security standardization is difficult due to the complexity of maintaining security properties throughout the lifetime of a standardization process, there is a clear use-case for formal modeling.

The general insight behind formal modeling is that the traditional method of discovering new attacks on security APIs (and security protocols in general), by being based on human insight, may miss important attacks. While a single human may be able to discover by sheer insight an important attack, the state-space of possible combinations of items such as keys, messages, cryptographic primitives, and various desired properties may simply be difficult to discern without the assistance of automated or semi-automated tools. Similar to the automated discovery of proofs, the ideal automatic security checker would essentially be a “machine attacker” that would try out an large number of attacks using all possible combinations of cryptographic primitives and their parameters over messages in all possible states. The general technique is the reduction of maintaining security properties to a boolean satisfiability problem (SAT), where a model-checker is used to see if the security properties hold via automatically checking the property exhaustively (rather than theorem-proving) [18]. Although the problem is well-known to be undecidable, efficient SAT solvers exist for large classes of problem. Once a problem is detected via formal modeling, it may be fixed in the standard before deployment. If the standard has already been implemented, the flaw is usually then tested against real-world implementations, hopefully to be fixed once the flaw is shown to be valid.

This approach of formal modeling has shown itself to be successful against many already deployed protocols, in particular against TLS 1.2 [10]. Sometimes attacks on standards incorporate errors in the choice of cryptographic primitives, which are usually widespread in standardization as the time it takes to update. While usually the choice of a vulnerable cryptographic primitives is easily discovered, attacks on the protocol itself can be discovered years after the release of the protocol [9] due to fundamental problems in the protocol such as the lack of a well-defined state machine.

One area where formal modeling is just beginning to be applied to in standardization is in security API design. A security API consists of a set of functions that are offered to some other program that uphold some security properties, regardless of the program making the function calls and what functions are called [13]. For example, one would hope that an API like PKCS#11 that provides access to key material in hardware tokens would prevent any private key material from being tampered with, regardless of the application [17]. These kinds of security properties are particularly critical in many applications, and classically security APIs have been studied in the realm of hardware security modules [13].

Early work did not use generalizable formal techniques, but customized each technique for the API at hand [13]. Only more recently has fully automated analysis in terms of model-checking and theorem-proving been deployed, usually based on the Dolev-Yao (DY) abstract model where cryptographic primitives are given as functions on bitstrings in an abstract algebra [19]. This methodology has shown to be successful by its ability to compromise from non-standardized solutions such as an authentication server and steal private keys from the Yubikey USB hardware token [27]. Formal modeling has then be used to successfully reveal a number of API-based attacks on standards, including the commercially available tamper-resistant hardware security tokens PKCS#11 [17]. Currently, a large number of security APIs are under process of standardization at the IETF and W3C. Although formal modeling is not part of the current required security review of protocols in the IETF and the optional security review of protocols in the W3C, we believe it should be encouraged in the future as a mandatory part of the security review before and after implementation.

3 Background

In Sect. 3.1 we give relevant background on Javascript Web Cryptography. Section 3.2 reviews the existing academic literature on formal modeling that serves as the basis of our work on the Web Cryptography API, as well as mentioning previous usages of formal modeling for security properties on the Web. Section 3.3 summarizes the W3C Web Cryptography API (abbreviated as the “Web Cryptography API”).

3.1 Javascript Cryptography

As an increasing number of applications transition to the Web, the need of ordinary users to have more secure Web applications has increased and Web developers are attempting to match those expectations. Although there was initial hostility to the idea of cryptography in Javascript as exemplified by “Javascript Cryptography Considered Harmful,”Footnote 2 there has nonetheless been widespread interest in creating secure Web applications [21]. Yet without the proper cryptographic primitives working cross-browser, Javascript cryptography would indeed be dangerous. For example, the initial version of the ‘Crypto.cat’ encrypted chat application initially not only recreated their own cryptographic routines in Javascript but also deployed these Javascript libraries insecurely.Footnote 3 In a remarkable turn-around, Crypto.cat has since become the first formally verified Javascript-based cryptographic application. Although a number of well-designed Javascript cryptographic libraries exist such as the Stanford Javascript Crypto Library [38], there are certain properties even the most well-designed Javascript cryptography library presents, such as the problem of accessing the library itself securely. Although well-designed libraries can prevent this, common libraries OpenPGP.js Footnote 4 are vulnerable to side-channel attacks and critically use built-in weak number generation given by default by Math.random.Footnote 5 Furthermore, even well-designed libraries that feature native Javascript password-based key derivation using algorithms such as PBKDF2 are still simply too slow for widespread high security deployment (i.e. if a sufficient number of iterations are used). After a public workshop in 2012,Footnote 6 the W3C decided to create a cross-browser Web Cryptography API that would offer a number of standardized, constant-time primitives to be accessed by Web developers. This API does not address larger concerns with the Web Security Model, such as cross-origin code injection (as currently addressed by the Web Application Security GroupFootnote 7) and completely trusted servers (i.e. Javascript as remote code execution), as well as problems inherent in Javascript itself such as prototype inheritance and the lack of availability of efficient big integer operations.

3.2 Formal Modeling Literature Review

There is still no single dominant formal modeling language for modeling security. Alloy [22], a language based on the Z specification language that uses SAT solving, has been popular and used against APIs such as the Trusted Platform Module 1.2 API [40]. It has recently been used for discovering security vulnerabilities in Web applications, although it was not used to investigate the properties of the Web Cryptography API [30]. Alloy is a well-developed framework that allows infinite models. Scyther can work with an unbounded number of sessions but does not allow the modeling of control flows [16]. ProVerif is a cryptographic protocol verifier that works as a sequence of Horn clause and allows unbounded verification on smaller protocols [11]. Tamarin also provides unbounded session support with the required mutable global state [36].

AVISPA provides automatic validation and verification of security protocols based on the DY formalism given by re-writing rules, where the knowledge of the attacker can also be modeled using standard re-write rules rather than an entirely different set of rules based on, for example, belief logic. AVISPA supports multiple model-checkers over bounded sessions, and features both high and low-level formats for specifying protocols. Although unbounded sessions are of interest for some scenarios, given that in our scenarios the Web application operates over bounded sessions given the ephemeral nature of Javascript sessions (with the exception of ‘cookies’). We chose AVISPA for our analysis since it takes into account mutable global state shared between sessions, i.e. in particular keys in a key store that have attributes that change over time and that affect the execution semantics of protocols for operations such as signing and encryption in an API.

Earlier work in formal analysis of the Web did conceptual work such as dividing the attacker spaces of web attackers, who attack Javascript run-time environments in the browser via cross-site scripting (XSS) attacks, from network attackers who would attack the underlying TCP/IP connections between sites and attack the certificate authority infrastructure [2]. More recent work has used Proverif to model the properties of so-called “safe” cloud storage providers via the Web [4], verifying subsets of Javascript [39], and interactive proofs of security properties of Web applications [30]. However, none of these previous works were aimed at the Web Cryptography API. This paper presents the first security analysis and formal modeling of the Web Cryptography API.

3.3 W3C Web Cryptography API

The Web Cryptography API is a low-level API that exposes cryptographic functionality via a number of components specified as a WebIDL. A WebIDL is a way of specifying Javascript functions, although it may also in principle be bound to programming languages outside Javascript.Footnote 8 The main features of the Web Cryptography API are as follows, with much more detail given in the specification itself [3]:

  1. 1.

    RandomSource: Pseudorandom number generation.

  2. 2.

    CryptoKey: JSON object for key material.

  3. 3.

    CryptoOperation: Functions such as encryption and wrapping, along with error codes.

RandomSource. The RandomSource interface represents an interface to a cryptographically strong pseudo-random number generator (PRNG). Implementations should generate cryptographically random values using well-established cryptographic pseudo-random number generators seeded with high-quality entropy. Currently it provides no lower-bound on the information theoretic entropy present in cryptographically random values, but implementations should make a best effort to provide as much entropy as practicable and may provide platform or application specific entropy-related error messages.

CryptoKey. The CryptoKey object represents an opaque reference to keying material that is managed by the user agent. There are three types of keys: secret keys (for symmetric encryption), public keys, and private keys (for asymmetric encryption). Most importantly, the API does not expose key material itself, but instead only pass handlers to the key material itself in Javascript and so access to secret key material is forbidden. The only exception is when a key is explicitly given a boolean extractable set to true and then exported (even then, it would have the same-origin and structured clone properties). Keys that are not marked explicitly as private, secret, or as non-extractable (i.e. extractable set to false) will be accessible to the server with same-origin policy if key export is done. A simplified (types not being given for all values) Javascript WebIDL interface for CryptoKeys is given in Fig. 1.

Fig. 1.
figure 1

CryptoKey WebIDL

In the Web Cryptography API, we use the structured clone algorithm to store keys.Footnote 9 This algorithm is an abstraction on top of existing Web storage mechanisms such as IndexedDB Footnote 10 that has the same lifetime guarantees as the rest of Web storage. This would allow a user to clear their key material at the same time they ‘wipe’ cookies from their browser storage. So keys are restricted to the same origin policy in storage and are essentially ephemeral as they can be removed when session state is cleared.

CryptoOperation. The CryptoOperation is the heart of every cryptographic primitive. Given a algorithm and a set of parameters (usually including a handler to a key), the CryptoOperation will attempt to commit some operation. Every CryptoOperation can be thought of as a named finite state machine with an internal state, an associated algorithm, an internal count of available bytes, and a list of pending data. Every member of the list of pending data represents data that should undergo the associated cryptographic transformation if the operation as a whole is successful. The order of items when added to the list is preserved in processing, so that the first data that is added being the data processed. If the cryptographic operation fails (such as when the key type is wrong or when the algorithm is not supported), the CryptoOperation then terminates and produces an error code. A simplified (no types) Javascript WebIDL interface for CryptoOperations is given in Fig. 2. Each algorithm then gives support for a number of operations as given in Table 1.

Fig. 2.
figure 2

CryptoOperation WebIDL

Table 1. CryptoOperations per Algorithm
Fig. 3.
figure 3

Public Key signature example

Examples may clarify the usage of the API. An example generate a signing key pair and sign some data is given in Fig. 3. More examples, including symmetric key encryption, are given in the specification [3].

Supported Algorithms. Each algorithm type is given by the CryptoOperation and the key generation. Keys generated with particular algorithms thus can have their usages restricted to only those CryptoOperations permitted by the algorithm. We expect the Web Cryptography Working Group to be maintained over the long-term by the W3C, any requests for new algorithms can be sent to the Working Group for consideration and discussion with implementers. As the API is meant to be extensible in order to keep up with future developments within cryptography and to provide flexibility, there are no strictly required algorithms. However, in order to promote interoperability for developers, there are a number of algorithms that the API supports by default: RSA-PSS, RSA-OAEP, ECDSA, AES-CTR, AES-CMAC, AES-CFB, AES-KW, AES-CBC, HMAC, PKCS-v3 Diffie-Hellman (DH), the SHA family, CONCAT, HKDF-CTR, and PBKDF2. RSAES-PKCS1-v1_5 was supported but removed due to attacks described in this paper, see Sect. 5. These will be tested in the test-suite of the Web Cryptography API so developers will be able to easily ascertain with certainty if they can use these operations across browsers.

4 Formal Analysis

4.1 Threat Model

The threat model needs to be realistic in terms of actual attacks on the Web, and not too powerful. If we assume the origin is completely untrusted or compromised by an attacker, then the attacker can easily steal the application’s secrets directly before they are encrypted. Thus, we assume the origin is trusted when the WebCrypto API is initialized and secrets are successfully encrypted and stored on the client.

Our threat model is then a temporary compromise of the Javascript environment being used by the server or client after secrets have been encrypted by WebCrypto and stored on the client. This accurately models most cross-site scripting (XSS) attacks on the Web, including DOM-based attacks on the client and temporary compromises of Javascript delivered by the server.

The security property that we want to maintain is that access to the raw key material that is private, secret, or explicitly typed as non-extractable should not be accessible to Javascript. These keys should only be accessible to a server with same-origin policy if key export is explicitly done to extractable key material.

The goal of the attacker is to retrieve previously encrypted secrets. This threat model’s assumptions are built into our formalization, as seen from the rule definitions in Fig. 4. The inputs and outputs to each rule are either known by the attacker or stored on the client device.

Fig. 4.
figure 4

Model for each API call. Note that all usages are allowed for created and imported keys, simplifying the model and giving the advantage to the attacker.

4.2 Model

The models we used were constructed using the AVISPA toolset,Footnote 11 which was built to enable easy translation from protocol to model. The AVISPA toolset forms a hierarchical set of languages which take in a high-level protocol description and translate it through a series of steps to a low level description that functions as input to a model checking engine. Since AVISPA’s high level language is tailored towards protocols and not API’s, we designed our models in AVISPA’s intermediate format (IF). AVISPA’s IF format describes protocols modeled as an infinite state machine whose semantics is given via set re-writing.Footnote 12 Protocols are described unambiguously by sets of typed predicates which define states and rules which define state transitions. For example a predicate might take the following form:

figure a

Which represents a fact-type predicate relating to a variable K of type key. States are defined by a list of applicable predicates. Transition rules take the form of having a list of predicates on the left hand side which must be true for the transition to occur. The right hand side lists predicates which are true following the transition. The following shows an example rule which models encryption:Footnote 13

figure b

Initial states are described by declaring initial terms and predicates on them. Lowercase letters are used to represent instantiated terms. Uppercase letters denote free terms that may be bound to instance of the same type.

figure c

Initial predicates use instantiated terms:

figure d

This example would initialize a state machine with the predicates keystore(k) and \(private\_data(m)\). The \(do\_encrypt\) rule is applicable when \(M=m\) and \(K=k\).

AVISPA assumes an attacker following the standard DY model (where the attacker is called the “intruder”) and is represented functionally by an iknows predicate which dictates information known to the attacker. Further, the attacker has basic cryptographic capabilities. For example, the following rules would be applicable to the attacker independently of the modeled protocol:

figure e

Consistent with the DY model, information communicated over the channel between actors is predicated with iknows. Thus, inputs to rules may be attacker created values and outputs are assumed to be learned to the by the attacker. This paradigm allows us to model compromised Javascript, where inputs may come from any source and outputs may be sent anywhere. The only state accessible to the API is the keys stored on the host, which we modeled with a keystore predicate. The attacker in this model uses keys stored on the host. Our API rules use iknows or keystore to predicate inputs:

figure f

The attacker goal states specify the conditions of a successful attack. For example, an attacker goal when testing confidentiality would be defined as a state in which both the iknows predicate applies to a variable already declared secret by the secret predicate, for example:

figure g

4.3 API Model

To test properties of the API, we built a general API model which we then varied slightly to perform different tests. Creation of the general model includes custom predicates, transition rules representing API calls, and handling of key objects. The API call transition rules are built from both AVISPA’s default predicates (crypt, scrypt, iknows, etc.) and custom predicates. The modeling for each rule is described in Fig. 4.

In addition to AVISPA’s default predicates, several custom predicates were necessary to handle the modeling of key objects. The actual CryptoKey objects associates raw key data and the following set of attributes:

figure h

Our modeled CryptoKey objects only represent the parts of the actual CryptoKey object. For efficiency reasons, our model expresses keys as (type, value) pairs. A key’s attributes (extractable, usages) are represented by inclusion of that key in a set representing the particular attribute. For example, all keys with the encrypt usages are contained in a set named Javascript_encrypt. We ignore the algorithm attribute in our model.

Each entity is associated with a store of keys known to that entity. Each WebCrypto operation requires that the keys it will use be present in its associated entity’s key store. Some operations (generate, import, unwrap) will add a key to the key store.

WebCrypto calls were translated directly into transition rules for our model. The predicates used are a combination of AVISPA defined (crypt, scrypt, iknows, etc.) and some that were specifically defined for this model. The predicates we defined are:

figure i

Modeling Specific Scenarios. Each individual scenario was created by customizing the models initial state and attack goal. After this step is done, the discovery of attacks is then fully automated by AVISPA. Some scenarios also included additional transition rules which allow more control over the behavior of the model. The additional rules serve as “unit operations” for each scenario. These operations model the equivalent of a sequence of individual API operations. Building unit operations for each test had two advantages. First, it optimizes the number of steps needed by the model checker in order to find attack sequences that include this sequence of steps. Second, constraints can be added to the model which require any found attack sequences to contain these operations. This allows modeling a scenario with the requirement that either the server or client fulfilled their role properly. A large number of scenarios were formalized, building up from simple to more complex in terms of properties by the use of these unit operations.

As an example, we look at the model used to check confidentiality of wrapped key exchange messages sent from client to server. This model is initialized with three key objects. The intent is to model two keys that belong to the client: one (swkey) for wrapping and the other (skey) to be exchanged securely. The third (ikey) key is known to the attacker and can be used in whatever way aids the attacker:

figure j

The predicates in the initial state describe the properties of the keys using the predicates as described earlier. The goal state for this case was described by:

figure k

This goal specifies that for some variable key K, K has been defined to be both secret and known by the attacker. This goal was trivially achieved because extract(skey) lets a secret key be marked as extractable which allows the attacker to export skey and learn its value.

To force the model to find attack sequences that show how export attacks can effect operations such as key exchange with the key being explicitly extractable (as would be the case with secret key material by default), we modified our model slightly. First, we remove extract(skey) from the initial state. Next we added a \(c\_send()\) unit operation which wraps and sends a key without requiring either keys to be extractable:

figure l

The \(has\_sent\) fact is used to force this rule to be used. This is accomplished by modifying the goal state to be require that \(has\_sent(K)\) be true, which can only happen after the \(c\_send\) rule is used:

figure m

The attack found by the model checker for this set of modification is discussed in Sect. 4.4.

4.4 Tests and Results

We tested security properties by systematically modeling different use cases and assessing the resulting attacks. The attacks we found existed due to potentially unintuitive traits of the API, which would have negative security implications if misunderstood by a large audience. The interesting attacks fell into two types:

  • Export Attack: Exporting extractable key data and changing usages.

  • API Attacks: Using client API calls to recover clear text of encrypted communication via an attack on key wrapping.

To summarize, our analysis found that keys managed by the API, if wrapped and then unwrapped, then lose their usage properties. In particular this can be used to subvert operations such as key exchange and so reveal private key material.

Export Attack. While unextractable keys are appear safe, our attack shows there are no safeguards in place to preserve the usage attributes on extractable keys. Furthermore, any wrapped key can be unwrapped and then given arbitrary usage attributes. Thus, there is no guarantee that a key transmitted by wrapping will be used with the intended usages.

The test that revealed this property was modeled with a client initialized with two symmetric keys. One was an unextractable key with the wrap and unwrap usage enabled. The other key was extractable but had no usages enabled. The initial state and goal state are given below, where skey is the secret key and ikey is the key being under possession of the attacker (note that i is used as the “attacker” is called “the intruder” in AVISPA):

figure n

Not only the encrypt usage, but all usages could be added simply by wrapping and unwrapping the extractable key: wrap(skeyikey), unwrap(skeyikey). This simple single-host attack extends to wrapped keys transmitted between multiple hosts, and demonstrates the lack of control over usages: Once a key has been wrapped, the original usages with which it was created are lost, and new usages, as well as the choice to designate a key extractable, can be added during the unwrap operation.

Key Exchange API Attacks. The test case in Sect. 4.4 revealed the lack of key attribute preservation, and an attacker can be successful in deploying this strategy to reveal secret key material in key exchange and message passing protocols that use the WebCrypto API. A set of experiments, also done with the AVISPA model, involved keys sent between a client and server using various combinations of authentication and key wrapping.

Enumerating these cases also gives us insight into the security of general message exchanges based on WebCrypto: As key wrapping is a composition of export and encrypt, if an attack existed on a wrapped key, then the same attack would apply to an encrypted message. The combinations of encryption and authentication our model discovered compromises in are:  

Symmetric encryption :

– The sender wraps the key using a symmetric key shared with the receiver who unwraps the key

Asymmetric encryption :

– The sender wraps the key using public key for the receiver who unwraps with the corresponding private key

Symmetric encryption with asymmetric signing :

– The symmetric encryption case augmented by signing with the sender’s private key

Asymmetric encryption with asymmetric signing :

– The asymmetric encryption case augmented by signing with the sender’s private key

 

Each test was initialized with enough keys to allow the client and server’s task to be modeled as well as the attacker. We modeled multiple versions of each scenario: one matching the current API specification and a second restricted version designed to show changes that could reduce attacks. The attacks are described in a number of tables. Operations in the attack sequences are prepended with an identifier specifying the entity that performed the operation: ijs- malicious Javascript controlled by the attacker, i- the attacker, c- the client Javascript running honestly, and s- the honest server.

Table 2 shows attacks found by testing confidentiality of keys sent from client to server. A successful attack involves the attacker learning a key that was also defined as secret. In the cases using symmetric encryption, the basic model used a symmetric wrapping key that had both wrap and unwrap usages enabled. These cases allowed API attacks where the secret key was unwrapped and given export privileges and then extracted. The restricted cases were modeled by removing the unwrap usage from the client’s wrapping key, which removed this attack as well as the export attack on the key. The asymmetric case did allow export attacks but not API attacks.

Table 3 covers confidentiality attacks but this time for keys sent from server to client. In these scenarios all base cases were susceptible to an API attack which caused the key received from the server to be imported as extractable and then immediately exported. No modifications were found which prevented this attack.

Table 2. Client \(\rightarrow \) Server confidentiality attacks
Table 3. Server \(\rightarrow \) Client confidentiality attacks

Table 4 shows integrity attacks on the same set of scenarios as Table 2. The successful attack was modeled as a key, originally known only to the attacker, being stored in the server’s key store. For most cases, both symmetric and asymmetric, API attacks allowed an attacker to send a key to the server by importing that key into the client and using API calls to wrap and possibly sign the key. The only modification we found preventing this attack was to disallow use of one of the keys, but this may not be practical in real world use cases.

The integrity attacks shown in Table 5 on keys sent from server to client yield fewer API attacks. API attacks exist for the cases where the attacker has access to the wrapping key. This is the symmetric case where the client’s key has wrap and unwrap usages as well as the asymmetric case where the encryption key is public by default. With authentication required, no API attacks were found.

Table 4. Client \(\rightarrow \) Server integrity attacks
Table 5. Server \(\rightarrow \) Client integrity attacks.

These results lead to a few general observations. Export attacks are often available because keys that can be wrapped are also then extractable; any key that can be exported from the client can be retrieved in the clear by an attacker even though the wrapping is intended to keep the key secret. The found API attacks have a common element of using a key stored on the client to perform cryptographic operations. Some of these attacks are caused by the fact that the extractable attribute and usages array are not preserved for wrapped keys, and unwrapped keys can be given any new combination of attributes, including extractable. Other attacks could be mitigated by limiting the usability of stored keys. For example in the symmetric encryption case, if one key is used for both directions, the attacker can use the client’s keys to both encrypt and decrypt the communication. However, using distinct keys for each direction of communication and reinforcing this behavior with usages attributes prevents this type of attack assuming the usages are not changed. Thus, the successful API attacks could be prevented if usages were bound to key material in general and not allowed to be altered while the key is being stored. Lastly, authenticating via asymmetric keys where extractability of key material is not allowed prevents the attacks on confidentiality and integrity of keys from the server to the client.

5 Algorithm-Level Analysis

In our formal analysis, we treated algorithms as “black boxes” in the analysis of cryptographic primitives. This is because some of the attacks on security APIs are beyond the scope of the DY model employed by AVISPA. For example, formal models do not in general deal with attacks like oracle attacks that observe the error messages that are returned by the API. Furthermore, some algorithms have well-known weaknesses.

In this review, we limit ourselves to peer-reviewed results on the algorithms which have been included in the first Candidate Recommendation version of the WebCrypto API, although the precise algorithms are still in flux due to interoperability testing. Table 6 summarizes the results. Although none of these results or attacks are new in terms of cryptanalysis, the fact that they were present in the WebCrypto API should be explicitly noted. After this analysis, RSAES-PKCS1-v1_5 was removed from the specification and the problems with padding error return codes were corrected.

There is at least one annual publication, the ENISA “Algorithms, Key Size and Parameters Report,” whose aim is to track ongoing developments, which discusses a much larger set of algorithms in much greater depth. Our results are in general the same except for algorithms ENISA does not cover like PBKDF2 and AES-KW [37].Footnote 14 We note that HKDF has security proofs [26] but needs more study. Security models for password-based key derivation functions are still in a state of flux [42]. PBKDF2 has known weaknesses [43], and many implementations do not use enough iterations.

Table 6. Algorithm summary

In detail, the main problematic algorithm originally included in WebCrypto was RSAES-PKCS1-v1_5, which has been known to be vulnerable to a chosen ciphertext attack (CCA) since 1998 [12]. The attack has recently been improved to require a median of less than 15 000 chosen ciphertexts on the standard oracle [5]. Instances of the attack in widely-deployed real-world systems continue to be found [23]. Finally, note also that as of version 1.3, RSAES-PKCS1-v1_5 will be dropped from the TLS standard.Footnote 15 In terms of alternatives, there are no publicly known attacks on RSASSA-PKCS1-v1_5 but no security proofs and no advantages compared to other RSA-based schemes, while RSA-PSS has a security proof due to Bellare and Rogaway [8] in the random oracle model.

There are also some inevitable issues with elliptic curve cryptography, which is in an ongoing state of flux in both WebCrypto and wider internet standards. In particular, ECDSA has some provable security results but only in weak models [42]. There is debate on elliptic curves.Footnote 16 ECDH has provable security results [14], but like other plain DH modes it offers no authenticity, so this must be handled separately. A proposal exists to include Curve25519 [32] after the browsers are finished implementing the CFRG recommendations. In general, we recommend using only named curves with wide public review.

In terms of AES, there are well-known issues with AES-CBC mode that are not currently believed to pose a practical threat [25], and it is not CCA secure. Both AES-CBC and AES-CFB are secure against chosen plaintext attacks (CPA-secure) if the IV is random, but not if the IV is a nonce [35]. In particular AES-CFB does not tolerate a padding oracle [41] - indeed, in practice, padding oracle attacks are common [29, 31, 33]. The padding mode [24] is exactly that which gives rise to most of these attacks. AES-KW has received various criticisms, for example being inconsistent in its notions of security (requiring IND-CCA from a deterministic mode), but though it has no public security proof, it has no known attacks either [34]. AES-CTR is probably the best mode of the traditional AES modes, although the mode is easy to mis-use and thus in general AES-GCM should be preferred (ideally with an explicit safeguard to prevent re-usage of the IV). Since WebCrypto does not contain guidance on composing AES modes with a MAC and does not prevent the re-usage of an IV, care needs to be taken by developers.

Table 7. Explanation of padding attacks

Due to the inclusion of AES-CBC and the consideration of RSAES-PKCS1-v1.5, padding attacks against these protocols would be a threat to both encrypted messages and wrapped keys in WebCrypto. Table 7 explains how these vulnerabilities manifest themselves in the Webcrypto API. After these attacks were discussed with the W3C Web Cryptography Working Group due to the analysis presented in this paper, RSAES-PKCS1-v1_5 had its support removed from the W3C Web Cryptography specification. Also, errors that could lead to attacks on AES-CBC wrapped keys, such as DataError, were removed from the spec where necessary and replaced with OperationError that could not distinguish between a key and padding operation. This should be considered a good example of a standards-based Working Group working well with knowledge from the cryptographic community.

5.1 AES-CBC Wrapped Keys

It is worth noting that despite the API’s resistance to padding attacks against AES-CBC wrapped keys, this vulnerability could easily emerge through implementation errors or misuse of the API. To guard against implementation errors, we recommend the following checks:

  • All errors caused by improper padding or incorrect key length/formatting are indistinguishable. (Padding errors will be returned from a different subroutine than the other errors and be discovered first, so any information about the source of the error is potentially a distinguishing factor.)

  • Lengths of unwrapped keys are verified to match one of the predefined key lengths.

  • All bytes of padding are checked for conformance.

Of these three recommendations, the first was accepted in to the specification. Additionally, the specific key lengths reduce the search space of a brute force attack against 192 and 256 bit keys. Unwrapping a 256 bit key as if it was 192 bits requires guessing only the 64 bits that need to be (wrongly) interpreted as padding for unwrapping to be successful. Thus the problem is reduced to finding a 192 bit key. These, in turn, require guessing another 64 bits in order to be unwrapped as if they were 128 bit keys. From there, the problem is equivalent finding a 128 bit key. Thus, brute forcing 192 and 256 bit keys takes at most \(2^{128}+2^{64}\) and \(2^{128}+2^{65}\) guesses respectively, which is less than the traditional brute force attack. Lastly, it should be mentioned that if the attacker is given an oracle that uses the decrypt operation instead of the unwrap operation with the same key used for wrapping, a standard padding attack may be able to recover wrapped keys.

5.2 High-Level API Recommendations

Although the API does not provide “safe” defaults, the IRTF CFRG (CryptoForum Research Group) created a document to track known security flaws, attacks, and the status of formal security proofs for each algorithm in the API.Footnote 17 From our analysis, it is quite clear what the recommend modes should be in general for a developer-friendly “high-level” API that also automatically took care of IV vector initialization and other parameters. For RSA-based algorithms, RSA-PSS should be used for signing and verification while RSA-OAEP should be used for encryption and decryption. It is likely that Curve 25519 support should be added. Standardised by NIST, AES-GCM is gaining traction in standards such as IPsec, MACSec, P1619.1, and TLS [35]. Regarding DH, more protocols are now favoring ECDH as attacks against “weak” standard Diffie-Hellman groups are not as powerful against elliptic curves due to a loss of a clear precomputation-based advantage [1]. HMAC has well-studied security proofs, even if the underlying hash function is not (weak) collision resistant [7]. In terms of hashing functions, of course SHA-2 is to be preferred due to the amount of increased feasibility of practical methods of obtaining collisions for SHA-1.Footnote 18 As regard key size, in-line with NIST and ENISA [37], larger key sizes should be preferred such as RSA keys of at least 2048 bits and 256 bits for symmetric keys and elliptic curve cryptography.

6 Conclusions

6.1 Fixing the Web Cryptography API

In summary, the Web Cryptography API had three attacks, of which only one still stands. The attack that is still present is that the usages of keys are not preserved upon export that can be exploited in numerous ways to reveal not only wrapped secret key material sent from between the client and server but also disrupt authenticated key exchange. A number of simple mitigations would prevent this attack. The most general solution would be to prevent usages from being changed, but this binds key usages to a key throughout its lifespan. A more limited mitigation that would address only the unique case of wrapping would be to have key wrapping require that the properties of a wrapped and then unwrapped key be preserved, and not require the export of the wrapped key before wrapping. Wrapping could be done outside the general Javascript environment and only the wrapped key material exposed. One way to implement this option would be to inherit the property of being unextractable from the wrapping key to the wrapped key by default. Another more restrictive option would be to prevent wrapping and unwrapping. Earlier errors involving padding attacks being made possible due to error types were corrected, and the \(RSAES-PKCS1-v1\_5\) algorithm was correctly removed from the specification due to the analysis presented in this paper. However, the API does not suffer from the fatal errors in its key management that can be detected via formal modeling, such as PKCS#11 [17] or the Yubikey [27].

In detail, the handling of key attributes in the API does not create a clear intuition about their actual effect as the usages may not always be supported, and so will confuse developers about key management across the boundary between client and server. For any key transported between either client and server or server and client, the usages array may be changed arbitrarily. In other words, the originating host has no control over the usages a key has once imported onto another host. Another limitation is that keys are either extractable or not, and must be extractable in order to be wrapped. As demonstrated, extractable keys are easily attacked and can be retrieved (including maliciously) from a client with a single API call. Although seemingly harmless insofar as we would assume a correctly designed Web application would only allow keys to be extractable on purpose, this produces counter-intuitive results when mixed with wrapping, as restricting keys to be wrapped to be extractable forces the aforementioned vulnerabilities. This wrapping attack was verified in all conformant Web Crypto implementations, including Chrome, Edge, and FireFox. Furthermore, it prevents WebCrypto for being used for use-cases such as those proposed by Netflix to ensure secure delivery of key material to clients. This attack also prevents users from sharing long-term private keys that are unknown to the server between sessions by virtue of wrapping and sending to the server and then downloading the wrapped keys into private local storage when a successful authentication is completed. This is a widely requested feature for those wanting some ability to authenticate without the server being able to easily impersonate a user by having access to all the user’s secrets.

The lack of a long-term key storage model combined with a lack of persistent key usages may be detrimental to the usage of Web Cryptography. Without guidance, developers may make poor choices that do not meet expectations when storing key material, as the lifetime of these keys is tied to the execution environment. While this provides many positive security and privacy benefits, to retain a key for use in later sessions developers will need to make use of a persistent key storage service on the server using the previously described problematic key exporting and wrapping routines. As it would be expected then that key wrapping in order to send keys from the client to the server (and back again upon revisiting the page) will be used to preserve long-term keys, the key wrapping attacks mentioned earlier are particularly dangerous. One suggestion is that future versions of the specification should likely tie private keys and wrapping operations with special processing outside of the normal Javascript environment, or even more ambitiously try to use a trusted environment to secure keys and cryptographic operations. This may require some kind of tie between hardware tokens for keys and their operations. Recently, the W3C has been exploring adding hardware token access to the Web Cryptography API in their “Web Cryptography v.Next” workshop, and so the next version of the API may support both secure multi-session key storage and cryptographic operations on those keys via some form of a trusted execution environmentFootnote 19 as well as access via next-generation authentication APIs such as FIDOFootnote 20 to origin-bound platform-held keys via call-response requests that do not reveal the secret key material.Footnote 21

Standards to assure the end user of the integrity of Javascript code would prevent many of these attacks. Only recently has the W3C begun to develop standards to secure Javascript code, and these tend to be quite simple such as the Sub-resource Integrity W3C standard that allows the hash of Javascript to be checked before running [15] or Content Security Policy [6] that restricts the domain of Javascript being run. In detail, Sub-resource Integrity requires Javascript linked or imported as a script to match a particular hash before execution and so could prevent some of these cross-scripting attacks or where a third-party library has been exploited in order to gain access to the origin. There does not yet exist for Javascript a way to securely install code, such as has been done via signed code in Linux-based operating systems, much less the more comprehensive necessary precautions taken into account by The Update Framework.Footnote 22 While signed Javascript may seem difficult, many other systems such as native applications have moved to such a model and so it should not be surprising if the Web itself may need to adopt signed code. In fact, the hashes of popular Javascript code could even be imagined to be stored in a Merkle-tree based append-only log such as those being designed in Certificate Transparency [28]. Also, there does not exist a standard way to defend the entry in cleartext of data in locally-running Javascript from the server.

These kinds of attacks could also be countered by creating higher-level libraries that make it easier to use the Web Cryptography API and avoid having developers make decisions of key usages and key exporting. This design could be validated if there was a large-scale study of the usage of the Web Cryptography API amongst web developers attempting to solve common tasks with the API, with an eye towards common errors and mistakes with defaults and for attacks such as those detailed in this paper.

6.2 Next Steps for Standards Research

More formal research is needed on the larger framework of the Web Cryptography API and the Web security model, with a focus on the possible interactions between Web Cryptography and other APIs that are part of HTML5. Ideally, the entire Web Security Model needs to be formalized and modeled, and it only makes sense formalizing the security analysis of the Web Cryptography as part of this larger analysis as most applications will use multiple APIs with possibly contradictory security policies. It would make sense to engage in a thorough study to be able to determine important security properties such as safe key storage in both the specification and implementations thereof when the WebCrypto API is used in combination with other APIs that allow low-level access to a browser’s localstorage.

The process of formal modeling would be helpful if integrated into the standardization process to understand the security properties of APIs and their complex interactions with other APIs. One approach would be to include it at the early stages of the design of the standard. If it were, it could both correct early flaws, but would require considerable investment in updating the model. Another option would be do the formal model as part of the security review, although such a security review is currently optional at the W3C. Another option would be to include the formal modeling as part of the test-suite necessary to reach standardiation, where the test-suite must demonstrate security properties. One possible incentive structure is that just as currently W3C specifications require conformance testing via a test-suite to be done manually, the automatic generation of a test-suite using formal methods would both save the developers time and lead to a more thorough test-suite. The formally-generated test-suite could then be tested against real-world implementations in order to prove interoperability and conformance. The use of formal methods for testing is currently under development for the new Web Authentication API (formerly the “FIDO 2.0” API) that attempts to supplement passwords with one-factor cryptographic authentication.Footnote 23 In general, we hope that formal analysis of Web APIs will lead to a more secure Web that is better understood and easier to use for developers.