UC San Diego

Web applications are often responsible for sensitive user data, but areexceedingly difficult to secure. % On the backend, they lack effective tools to prevent data leakage, meanwhile bugs in the browser can compromise otherwise secure code. % While developers have improved this situation by employing informal bugfinding techniques such as fuzzing, new bugs are commonly discovered and exploited in the wild. % Formal verification tools promise to stem the tide of bugs, but they are difficult to use in practice; theorem provers are cumbersome while general-purpose automated verifiers fail to scale to real-world programs. % Domain-specific languages (DSLs) allow us to make automated verification tractable by ``baking in'' a particular verification problem to the language semantics. % In this dissertation we introduce three such DSLs designed to automatically provide security guarantees for web applications: % \begin{enumerate} \item \emph{CT-Wasm}, an extension to the WebAssembly type system which provides formally guaranteed protection against timing side-channel attacks. \item \emph{Scooter}, a domain-specific language which prevents server-side data leakage in database-backed applications. \item \emph{VeRA}, a subset of C++ which verifies the correctness of range analysis in Firefox. \end{enumerate}