Repository logo
 

Mechanising and evolving the formal semantics of WebAssembly: the Web's new low-level language

Simple item page
cam.restrictionthesis_access_open
cam.supervisorSewell, Peter
cam.thesis.confidentialfalse
cam.thesis.confidential-clearanceNone - this thesis does not contain confidential and / or sensitive information
cam.thesis.copyrightfalse
cam.thesis.copyright-clearanceNo copyright - this thesis does not include material with third party copyright
dc.contributor.authorWatt, Conrad
dc.contributor.orcidWatt, Conrad [0000-0002-0596-877X]
dc.date.accessioned2021-10-06T01:22:07Z
dc.date.available2021-10-06T01:22:07Z
dc.date.issued2021-11-27
dc.date.submitted2021-02-05
dc.description.abstractWebAssembly is the first new programming language to be supported natively by all major Web browsers since JavaScript. It is designed to be a natural low-level compilation target for languages such as C, C++, and Rust, enabling programs written in these languages to be compiled and executed efficiently on the Web. WebAssembly’s specification is managed by the W3C WebAssembly Working Group (made up of representatives from a number of major tech companies). Uniquely, the language is specified by way of a full pen-and-paper formal semantics. This thesis describes a number of ways in which I have both helped to shape the specification of WebAssembly, and built upon it. By mechanising the WebAssembly formal semantics in Isabelle/HOL while it was being drafted, I discovered a number of errors in the specification, drove the adoption of official corrections, and provided the first type soundness proof for the corrected language. This thesis also details a verified type checker and interpreter, and a security type system extension for cryptography primitives, all of which have been mechanised as extensions of my initial WebAssembly mechanisation. A major component of the thesis is my work on the specification of shared memory concurrency in Web languages: correcting and verifying properties of JavaScript’s existing relaxed memory model, and defining the WebAssembly-specific extensions to the corrected model which have been adopted as the basis of WebAssembly’s official threads specification. A number of deficiencies in the original JavaScript model are detailed. Some errors have been corrected, with the verified fixes officially adopted into subsequent editions of the language specification. However one discovered deficiency is fundamental to the model, an instance of the well-known "thin-air problem". My work demonstrates the value of formalisation and mechanisation in industrial programming language design, not only in discovering and correcting specification errors, but also in building confidence both in the correctness of the language’s design and in the design of proposed extensions.
dc.description.sponsorship2019 Google PhD Fellowship in Programming Technology and Software Engineering Peterhouse Research Fellowship
dc.identifier.doi10.17863/CAM.76476
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/329032
dc.language.isoeng
dc.publisher.collegeSt Catharines
dc.publisher.institutionUniversity of Cambridge
dc.rightsAttribution 4.0 International (CC BY 4.0)
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.subjectWebAssembly
dc.subjectmechanisation
dc.subjectIsabelle/HOL
dc.subjectvirtual machine
dc.subjectprogramming language semantics
dc.subjectWasmCert
dc.titleMechanising and evolving the formal semantics of WebAssembly: the Web's new low-level language
dc.typeThesis
dc.type.qualificationlevelDoctoral
dc.type.qualificationnameDoctor of Philosophy (PhD)
dc.type.qualificationtitlePhD in Computer Science
pubs.funder-project-idEngineering and Physical Sciences Research Council (1790117)
rioxxterms.licenseref.startdate2021-11-27
rioxxterms.licenseref.urihttps://creativecommons.org/licenses/by/4.0/
rioxxterms.typeThesis

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
thesis.pdf
Size:
1.49 MB
Format:
Adobe Portable Document Format
Description:
Thesis
Licence
https://creativecommons.org/licenses/by/4.0/
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
DepositLicenceAgreementv2.1.pdf
Size:
150.9 KB
Format:
Adobe Portable Document Format
Download

Collections

Theses - Computer Science and Technology