DEV Community

GeneLab_999
GeneLab_999

Posted on

Proving what a URL allowlist decides, in Lean 4

#security #ai #formalmethods

This article describes URLFence as of commit ea3c061 (CI: run 40618042270).

AI agents fetch web pages for you, and their tools are supposed to stay on an allowlist of hosts.
That kind of check ("is this URL's host allowed?") keeps going wrong in the same few ways, in agent
tools and elsewhere:

  • A string prefix or suffix instead of a hostname comparison.
    • CVE-2026-24052 (Claude Code WebFetch before 1.0.111) and CVE-2026-46341 (Apify MCP server before 0.9.21) used startsWith, so modelcontextprotocol.io.example.com and docs.apify.com.evil.com passed.
    • CVE-2026-33393 (Discourse's spam-host allowlist) used end_with? without a dot boundary, so attacker-example.com passed.
  • Userinfo taken for the host: CVE-2025-47241 (browser-use before 0.1.45).
  • Normalising before checking: CVE-2026-6322 (fast-uri before 3.1.2) decoded a percent-encoded @.

URLFence (https://github.com/hiroki-abe-58/urlfence) is a small Lean 4 library and CLI that makes
this decision, with theorems about what it decides.

What it does 

$ .lake/build/bin/urlfence check --allow docs.python.org --allow '*.example.com' -- https://docs.python.org/3/ https://docs.python.org.evil.com/ https://docs.python.org@evil.com/
{"input":"https://docs.python.org/3/","decision":"allow","scheme":"https","host":"docs.python.org","port":null}
{"input":"https://docs.python.org.evil.com/","decision":"deny","scheme":"https","host":"docs.python.org.evil.com","port":null}
{"input":"https://docs.python.org@evil.com/","decision":"reject","reason":"userinfo"}
Enter fullscreen mode Exit fullscreen mode

It fails closed. It accepts only a strict, canonical form of http(s) URLs and refuses
everything else with a reason:

  • whitespace, backslashes and non-ASCII characters;
  • uppercase letters in the scheme or host;
  • userinfo and percent signs in the authority;
  • IPv6 literals and IDNA xn-- labels;
  • browser-style shortcuts like https:/x, 127.1 or 0x7f.0.0.1.

That costs some convenience. In exchange, an accepted URL leaves little room for a second reading:
the proofs pin how URLFence reads it, and a test checks that Node's WHATWG parser agrees.

The theorems

  • parse_authority: in an accepted URL, the text from // up to the first /, ?, # or the end is exactly the host followed by an optional :port. isDelim_iff pins those three characters.
  • parseHost_chars: the host contains only a-z, 0-9, - and ., so it has no @, : or brackets to confuse anyone.
  • sub_matches_iff_render: a *.example.com pattern matches exactly when the host ends with . followed by example.com, which is the dot boundary the suffix bugs missed.
  • check_allow_iff: a URL is allowed iff it parses, its scheme is allowed, it matches an allowed pattern, and it matches no denied pattern.

The audit script requires 55 published theorems by name (22 for URLs, 33 for the address check
below). All of them depend only on Lean's standard
axioms, and each one is pinned together with the library definitions it depends on. The audit also
replays every module through Lean's kernel checker.

Tested against real parsers

The proofs are about URLFence's own parser. Whether a browser-grade parser reads the URL the same way
is a tested claim, not a proven one:

  • A differential test runs about 10,000 random and adversarial URLs, including printable ASCII characters inserted into hosts at random positions.
  • For every URL URLFence accepts, Node's WHATWG URL must report the same scheme, host and port, and no userinfo.
  • tests/compat.py goes further, on a fixed corpus of 41,647 boundary-heavy URLs (17,044 accepted). It compares how Python's urllib, urllib3, requests, curl and Node parse each accepted URL, and what they actually send: the Python clients and curl through a local proxy, and all five on their direct path (Node through http.request/https.request; fetch is not covered). There the harness redirects each connection the client opens to a fixture on 127.0.0.1 that records the host and port the client chose, the Host header (http) and the TLS server name from the ClientHello (https), then answers 403 or a fatal TLS alert; every connection goes to 127.0.0.1, so nothing leaves the machine. On the full corpus (Python 3.12.3, urllib3 2.0.7, requests 2.31.0, curl 8.5.0, Node 18.19.1) no client disagrees on scheme, host or port in any of the 15 views, and none reports userinfo in its parse or in an http request. One URL, https://b//yc%80a:;, is refused by urllib3 and requests when sending, so they send nothing. Not observed: DNS (nothing is resolved), whether the certificate is verified, and anything inside TLS; the harness hooks the clients, so it shows what each client chose, not what an unmodified client would do on a real network after DNS.
  • tests/mutants.py plants 26 plausible bugs one at a time: 15 in the URL check, 8 in the address check and 3 in the Node fetch example. They include the prefix and suffix mistakes, a wrong authority boundary and an IPv4 address read at the wrong offset. 22 break the build (18 in proof files, 4 in build-time examples; some only because a proof script no longer fits the changed code), one is caught by tests/test_addr.py, and the three in the Node example by tests/test_guarded_fetch_node.py.

GitHub Actions runs the audit, the registry check, the tests (with the runner's Node for the WHATWG comparison), a
fixed 1/16 subset of the client comparison and the mutation check on every push to main and on
every pull request. The full client comparison is a local run (python3 tests/compat.py).

Where the name resolves to

The URL check cannot know what an allowed name resolves to. A second command, urlfence addr,
checks resolved addresses against the IANA IPv4 and IPv6 special-purpose registries (as last updated
on 2025-10-09; that the Lean tables match IANA's files is checked by a script, not proven). It decodes
IPv4-mapped addresses, NAT64 addresses in a /96 prefix given with --nat64, and ISATAP
identifiers, and denies 6to4, Teredo and, unless configured, all of 64:ff9b::/96. 2026
advisories in MCP tooling and agent frameworks, among them auth-fetch-mcp (CVE-2026-49857), the MCP
Registry (CVE-2026-44430) and pydantic-ai (CVE-2026-48782), found address checks that missed
internal addresses written in an IPv6 form. The address theorems say that
every address in a registry row that is not globally reachable is denied (IPv4-mapped addresses
instead get the decision of the IPv4 address they carry), and that a denied IPv4 address stays
denied in each of those forms. The address parser is compared with inet_pton on 50,000 strings (for IPv4 its
reading is also proven).

examples/guarded_fetch.py pins by default: on every hop it resolves the host once, refuses if
any answer is denied, and connects only to a checked address, keeping the name for Host and TLS.
A proxy would resolve the name again, so while pinning the example refuses to use one.
examples/guarded_fetch.mjs does the same for Node's http/https.request (not fetch()): it
connects to the checked address on a socket it opens itself, so Node does no lookup of its own.

What it does not do

  • Unpinned clients: a client that resolves the name itself (a browser, curl, requests) or goes through a proxy is not covered by urlfence addr; pin the connection, or filter egress. The examples pin TCP connections only, not UDP or QUIC, and do not restrict ports.
  • Some IPv4-in-IPv6 schemes: addresses in unconfigured network-specific NAT64 prefixes, the other RFC 6052 prefix lengths, 6rd, MAP and SIIT-EAM are not decoded, so they are allowed as plain global addresses; deny such prefixes with --deny.
  • Your own networks: internal services on global addresses must be denied by you.
  • Redirects: urlfence check decides one URL; re-check every hop, as the examples do.
  • What the server does: open redirects and proxies on an allowed host are out of scope.
  • IPv6 and IDNA in URLs: both are refused.

Pair it with egress controls for the connection itself.

Try it 

git clone https://github.com/hiroki-abe-58/urlfence && cd urlfence
lake build              # builds the CLI here: .lake/build/bin/urlfence
./scripts/reproduce.sh   # fresh clone of HEAD: build, audit, registry check, tests, client comparison, mutants
Enter fullscreen mode Exit fullscreen mode

It needs git, elan, Python, Node, curl and openssl. To call it from your
own code, examples/guarded_fetch.py (or guarded_fetch.mjs for Node) shows the pattern: check the URL, request exactly the checked
string, check every resolved address and connect only to a checked one, and check every redirect
target before following it.

It is Apache-2.0. I started and lead the project; the code and proofs were written with
Claude Code (Claude Opus 5.5), and so far they have been reviewed only by AI, in separate Claude
sessions. No human has reviewed them yet, so reviews, counterexamples and issues are
welcome. The only guarantees are the theorems; the tests are evidence on the inputs they cover.

References

Writing disclosure: this article was drafted and fact-checked with AI assistance under my direction.

Top comments (0)