Verifying Google's Chromium
Dashboard with ESBMC
A reproducible proof-of-concept by Cyber-Reasoning Consultancy (CRC) applying ESBMC's Python frontend to chromium-dashboard, the Google App Engine backend behind Chrome Platform Status (chromestatus.com). ESBMC confirmed ten live API-validation findings; two were confirmed and fixed upstream by the chromium-dashboard maintainers at Google in PR #6451 and PR #6452. Sources, harness and run instructions are published in lucasccordeiro/chromium-dashboard-esbmc.
2 of 10
live findings already confirmed and fixed upstream by Google (PR #6451, PR #6452)
10
live API-validation findings confirmed by ESBMC counterexamples and reproduction
48
verification targets across five tiers, under 30 seconds end-to-end
2
security invariants formally proven sound, with non-vacuity controls
Context
chromium-dashboard is the Python backend that powers Chrome Platform Status: it manages Chrome feature proposals, origin trials, review gates, and the shipping decisions that move a web-platform feature through the process. Its HTTP API layer parses operator-supplied query parameters and request bodies, and a single unvalidated value, a milestone of zero, a falsy state code, a malformed range, can slip past the validators and surface as an opaque HTTP 500 rather than a clean 400.
We wanted to know whether ESBMC's Python frontend could reason about that input-validation logic directly, exhaustively, and on a developer laptop, and turn a class of "accepted-then-crashes" defects into findings that the Chrome team would accept and fix, while formally proving the parts that are already sound.
Approach
The harness pins chromium-dashboard at commit
d0d21c8
(2026-05-26) and drives ESBMC's Python frontend over
48 verification targets across five tiers, from pure arithmetic
helpers (is_weekday,
weekdays_between),
through HTTP API input-validation paths and self-certify boolean contracts, up to
review/approval security invariants and milestone arithmetic. Verification runs in
two phases, functional contracts expressed as assertions and an
--overflow-check
pass for CWE-190 (signed overflow) and CWE-369 (division-by-zero), and the full
make verify
sweep completes in under 30 seconds with zero failures.
Every candidate defect is paired with an ESBMC counterexample and an empirical reproduction against the running API, so that a finding is reported only when it is both a solver counterexample and an observable wrong response. The same discipline is applied in the other direction: where a property holds, ESBMC is used to prove it sound rather than merely fail to find a bug.
Results
Two findings confirmed and fixed upstream by Google. The
chromium-dashboard maintainer merged
PR #6451
("Give 400 for bad channel range"), resolving Finding A, a bare
ValueError
in api/channels_api.py
that returned HTTP 500 instead of 400 on a bad range, and
PR #6452
("Fix validation of 0 int parameters"), resolving Finding D, a falsy-value
validator bypass in api/reviews_api.py
where a state
of 0 slipped
past the check and crashed with an HTTP 500. Both were merged on 2026-06-03.
Ten live API-validation findings in total. Beyond the two fixes,
the findings were filed on the public tracker or carried as reproducible drafts:
?num=0
silently returning an empty page
(#6442),
?start=0/?end=0
returning null dates
(#6443),
and a missing feature_changes
key raising a KeyError
into an HTTP 500
(#6464),
among others. Each carries an ESBMC counterexample and a reproducing request.
Two security invariants formally proven sound. ESBMC proved the
gate-vote tally integrity in
internals/approval_defs.py:_calc_gate_state
and the vote-authorization logic in
api/reviews_api.py:require_permissions.
Each proof shipped with deliberately buggy controls that ESBMC catches,
confirming the proofs are non-vacuous rather than passing trivially.
One ESBMC toolchain fix. The PoC surfaced a bug in ESBMC's own
Python frontend, nondet_bool()
inside list comprehensions, which was fixed upstream in
esbmc/esbmc#5023
(merged 2026-06-01), the verification work feeding directly back into the
open-source tooling that made it possible.
What this means
The HTTP input-validation surface of a production Google web service is amenable to bounded model checking with ESBMC's Python frontend, at developer-laptop speeds and without a deployment in the loop. For teams operating or extending services like chromium-dashboard, the payoff is twofold: a class of "accepted-then-500" validation bugs can be turned into fast, deterministic checks that, as PR #6451 and PR #6452 show, the maintainers are willing to merge, and the parts that are already correct can be backed by a formal, non-vacuous proof rather than an absence of test failures.
References
- lucasccordeiro/chromium-dashboard-esbmc, public PoC repository (harness, witnesses, tiered targets, findings report). github.com/lucasccordeiro/chromium-dashboard-esbmc
- GoogleChrome/chromium-dashboard PR #6451, "Give 400 for bad channel range" (merged 2026-06-03); fixes Finding A. github.com/GoogleChrome/chromium-dashboard/pull/6451
- GoogleChrome/chromium-dashboard PR #6452, "Fix validation of 0 int parameters" (merged 2026-06-03); fixes Finding D. github.com/GoogleChrome/chromium-dashboard/pull/6452
- GoogleChrome/chromium-dashboard issues #6442, #6443, and #6464, further API-validation findings filed upstream. github.com/GoogleChrome/chromium-dashboard/issues/6464
- ESBMC, open-source bounded model checker, with the Python frontend used in this PoC. github.com/esbmc/esbmc
Note. This page describes an independent, reproducible proof-of-concept published by CRC's founder and ESBMC creator and lead developer, Prof. Lucas Cordeiro (University of Manchester). CRC Ltd is not in a commercial partnership with Google or the Chromium project, and the PoC was not commissioned by them; all reports and fixes went through chromium-dashboard's public issue tracker and pull requests. The harness is open source; every finding, witness and soundness proof, including the two fixes merged in PR #6451 and PR #6452, is reproducible from the public repository.