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: % $$\text{Unknown environment 'enumerate'}$$