Checking Cryptographic API Specifications in JavaScript. / Mitchell, Duncan.

2020.

Research output: ThesisDoctoral Thesis

Unpublished

Standard

Checking Cryptographic API Specifications in JavaScript. / Mitchell, Duncan.

2020.

Research output: ThesisDoctoral Thesis

Harvard

Mitchell, D 2020, 'Checking Cryptographic API Specifications in JavaScript', Ph.D., Royal Holloway, University of London.

APA

Vancouver

Author

BibTeX

@phdthesis{6d703414fc394ddebec18113493c33e0,
title = "Checking Cryptographic API Specifications in JavaScript",
abstract = "Increased awareness of privacy concerns on the Internet has encouraged developers towards implementing strong cryptography by default, in a trend dubbed {"}ubiquitous encryption{"}'. For instance, web applications for messaging platforms routinely implement client-side cryptography in JavaScript for true end-to-end encryption. The standardization of cryptographic APIs in JavaScript through the W3C Web Cryptography API, WebCrypto, has made strong cryptography available to non-expert web developers. However, cryptographic APIs are often hard to use correctly; the clash between the agile mindset of JavaScript developers and the requirements of secure software engineering leads to lingering problems. Further, JavaScript's dynamic types and often surprising semantics make it difficult to spot subtle security bugs, and such errors do not lead to failing test cases or visible errors.In this thesis, we propose an automatic mechanism for the detection of incorrect usage of cryptographic APIs in JavaScript. We introduce a system of Security Annotations: type-like tags which express security properties of values, e.g., whether a value is a ciphertext, or a cryptographically secure random value. Security Annotations are transparent to client code until they encounter an error, in which case the program under test fails. We formalize the notion of Security Annotations in a small lambda calculus, and use this to motivate the design of Security Annotations within an executable formal semantics for JavaScript. We construct a specification of the WebCrypto API and prove security guarantees in this setting. Finally, we implement Security Annotations within full JavaScript via source code instrumentation and use this to analyze both hand-crafted examples and real-world JavaScript applications.",
keywords = "Programming Languages, Security, Cryptography, Program Analysis, Symbolic Execution, JavaScript, WebCrypto, Security Annotations",
author = "Duncan Mitchell",
year = "2020",
language = "English",
school = "Royal Holloway, University of London",

}

RIS

TY - THES

T1 - Checking Cryptographic API Specifications in JavaScript

AU - Mitchell, Duncan

PY - 2020

Y1 - 2020

N2 - Increased awareness of privacy concerns on the Internet has encouraged developers towards implementing strong cryptography by default, in a trend dubbed "ubiquitous encryption"'. For instance, web applications for messaging platforms routinely implement client-side cryptography in JavaScript for true end-to-end encryption. The standardization of cryptographic APIs in JavaScript through the W3C Web Cryptography API, WebCrypto, has made strong cryptography available to non-expert web developers. However, cryptographic APIs are often hard to use correctly; the clash between the agile mindset of JavaScript developers and the requirements of secure software engineering leads to lingering problems. Further, JavaScript's dynamic types and often surprising semantics make it difficult to spot subtle security bugs, and such errors do not lead to failing test cases or visible errors.In this thesis, we propose an automatic mechanism for the detection of incorrect usage of cryptographic APIs in JavaScript. We introduce a system of Security Annotations: type-like tags which express security properties of values, e.g., whether a value is a ciphertext, or a cryptographically secure random value. Security Annotations are transparent to client code until they encounter an error, in which case the program under test fails. We formalize the notion of Security Annotations in a small lambda calculus, and use this to motivate the design of Security Annotations within an executable formal semantics for JavaScript. We construct a specification of the WebCrypto API and prove security guarantees in this setting. Finally, we implement Security Annotations within full JavaScript via source code instrumentation and use this to analyze both hand-crafted examples and real-world JavaScript applications.

AB - Increased awareness of privacy concerns on the Internet has encouraged developers towards implementing strong cryptography by default, in a trend dubbed "ubiquitous encryption"'. For instance, web applications for messaging platforms routinely implement client-side cryptography in JavaScript for true end-to-end encryption. The standardization of cryptographic APIs in JavaScript through the W3C Web Cryptography API, WebCrypto, has made strong cryptography available to non-expert web developers. However, cryptographic APIs are often hard to use correctly; the clash between the agile mindset of JavaScript developers and the requirements of secure software engineering leads to lingering problems. Further, JavaScript's dynamic types and often surprising semantics make it difficult to spot subtle security bugs, and such errors do not lead to failing test cases or visible errors.In this thesis, we propose an automatic mechanism for the detection of incorrect usage of cryptographic APIs in JavaScript. We introduce a system of Security Annotations: type-like tags which express security properties of values, e.g., whether a value is a ciphertext, or a cryptographically secure random value. Security Annotations are transparent to client code until they encounter an error, in which case the program under test fails. We formalize the notion of Security Annotations in a small lambda calculus, and use this to motivate the design of Security Annotations within an executable formal semantics for JavaScript. We construct a specification of the WebCrypto API and prove security guarantees in this setting. Finally, we implement Security Annotations within full JavaScript via source code instrumentation and use this to analyze both hand-crafted examples and real-world JavaScript applications.

KW - Programming Languages

KW - Security

KW - Cryptography

KW - Program Analysis

KW - Symbolic Execution

KW - JavaScript

KW - WebCrypto

KW - Security Annotations

M3 - Doctoral Thesis

ER -