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.
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.
Original language | English |
---|---|
Qualification | Ph.D. |
Awarding Institution |
|
Supervisors/Advisors |
|
Award date | 1 Mar 2020 |
Publication status | Unpublished - 2020 |
Keywords
- Programming Languages
- Security
- Cryptography
- Program Analysis
- Symbolic Execution
- JavaScript
- WebCrypto
- Security Annotations