Lecture 11: Ur/Web

What this lecture covers

Guest lecturer Adam Chlipala, the creator of Ur/Web, presents a language-based alternative to the string-and-filter approach to web security covered in earlier lectures. Instead of building HTML, SQL, and URLs as strings that get parsed and can be mis-parsed, Ur/Web represents them as typed, structured values that the compiler checks, which rules out entire classes of vulnerabilities by construction rather than by careful escaping.

After watching, you can explain why representing HTML, SQL, and URLs as strings is the root cause of injection-style vulnerabilities, describe how Ur/Web's type system and module encapsulation prevent cross-site scripting and unauthorized data access, and explain how the language automatically adds cryptographic protection against cross-site request forgery only when a handler actually depends on cookie state.

Key ideas

• Strings as the root problem: in mainstream frameworks, HTML, SQL, URLs, and JSON payloads are all strings; because the language does not understand their structure, values from untrusted sources can be misinterpreted as code, causing injection attacks.
• Typed HTML as a tree, not a string: Ur/Web builds pages as structured objects (via functions like tag and cdata), so untrusted text is inserted as text content and automatically escaped rather than parsed as markup.
• Abstract URL type: URLs are not plain strings; a value only becomes a URL after passing a bless function checked against an explicit allow-list policy, which prevents javascript: URLs and other unauthorized links.
• Typed SQL: database queries are checked against declared table schemas at compile time, and query results come back as native typed values instead of strings that must be parsed.
• Built-in transactions: each server-side function handling a client request runs its database operations as a single atomic transaction, simplifying reasoning about concurrency-related bugs.
• Module encapsulation: database tables and sensitive types (like user IDs and passwords) can be hidden inside a module, so other code can only interact with them through an approved interface, similar to an abstract data type.
• Automatic CSRF protection: the compiler detects when a request handler depends on implicit client-side context (such as a cookie) and automatically adds a cryptographically signed hidden form field, applied only where that dependency actually exists.

Walkthrough

Why Ur/Web exists (1:03)

Ur/Web is presented as a full-stack functional language (built on a new language called Ur) designed around three goals: programmer productivity, security, and performance, with the security goal central to this lecture. Its compiler understands what a web application should do well enough to catch mistakes a conventional language's compiler would miss, and benchmark results show it competitive in server-side performance with mainstream frameworks.

The mainstream model and where strings hide the risk (8:09)

The lecture sketches the conventional web application picture: browsers send HTTP requests with embedded URLs, servers respond with HTML strings containing more URLs, AJAX calls exchange XML/JSON strings, and JavaScript mutates a page via string-identified DOM nodes. Chlipala highlights that URLs, HTML, SQL, and AJAX payloads are all just strings in this model - the source of code injection attacks, since nothing in the language understands or restricts how those strings get interpreted.

Ur/Web's structured alternative and transactions (12:12)

In Ur/Web, a browser request effectively names a server-side function to call, and the response is a strongly typed document tree rather than an HTML string; links embed references to other callable functions, and database access uses typed SQL syntax trees returning native records. Server-side functions run inside a single database transaction per request, which the lecture connects to a class discussion about whether automatic transaction restarts (on deadlock) could be exploited, for example as a denial-of-service amplification vector or an unusual timing side channel.

Live demo: typed HTML and blocking XSS (25:24)

A "Hello World" Ur/Web program shows that URLs are generated automatically from function names, with no separate routing configuration. Chlipala demonstrates that XHTML syntax compiles down to function calls like tag and cdata that build a tree, and that inserting literal text (even something that looks like markup, such as <b>hello</b>) is always escaped and rendered as text - cross-site scripting is not possible through this path because there is no implicit string-to-markup interpretation step.

Blocking JavaScript URLs and typed SQL with encapsulation (31:32)

Attempting to use a javascript: URL fails because URLs must pass through the bless function against an explicit, whitelist-based policy defined in a configuration file; by default no URLs are allowed. The demo then builds a simple chat room application backed by SQL tables declared directly in the language, with queries checked against table schemas at compile time. Wrapping the database tables inside a module makes them private, so only the module's exposed functions (like listing rooms or posting a chat message) can touch that data - other code cannot read or forge access to the underlying tables.

CSRF protection and login with encapsulated user accounts (56:23)

A login system is built using abstract ID and password types that can only be created by explicit conversion functions, preventing code elsewhere from reading raw passwords out of the user table. Once a cookie is introduced to track the logged-in user, and a request handler starts depending on that cookie (directly or indirectly through a called module), the compiler automatically inserts a cryptographically signed hidden form field verifying the cookie's contents - CSRF protection appears only where a handler actually has implicit context to protect, and is absent (correctly) when no such context exists.

AJAX, URL remapping, and interfacing with JavaScript (1:10:50)

The lecture closes with a version of the chat demo that uses AJAX-style calls: client-side Ur/Web code is compiled to JavaScript and can invoke server functions using an RPC-style call embedded directly in the code rather than callbacks. URL paths generated by the compiler can be remapped via configuration rules. A foreign function interface lets Ur/Web call arbitrary JavaScript libraries, but doing so gives up the compiler's safety guarantees, so it should be used carefully.

Before you watch

• Watch the two preceding lectures on the same-origin policy and web application security (XSS, CSRF, content sanitization), since this lecture positions Ur/Web as a structural alternative to those string-sanitization defenses.
• The paper assigned as reading for this class introduces Ur/Web's design; some familiarity with static typing and functional programming concepts (as in Haskell or OCaml) helps but is not required to follow the demo.

Check your understanding

1. Why does Chlipala argue that representing HTML, SQL, and URLs as plain strings is the root cause of most web injection vulnerabilities?
2. How does the bless function and its allow-list policy prevent javascript: URLs from ever becoming a usable URL value in Ur/Web?
3. What does it mean that Ur/Web wraps each request handler's database operations in one transaction, and what new class of concurrency-related risk did students raise about automatic transaction restarts?
4. How does hiding a database table inside a module (as with the room and user account examples) prevent other parts of the application from bypassing intended access rules?
5. Why does the compiler add CSRF protection to some request handlers but not others, and what specific server-side dependency triggers that protection?