Skip to main content
All case studies
Developer infrastructure · Python · 2026

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; we filed seven of them as issues on Google's public tracker, and the chromium-dashboard maintainers fixed three of those upstream in PR #6451, PR #6452 and PR #6656. Sources, harness and run instructions are published in lucasccordeiro/chromium-dashboard-esbmc.

3 of 7

issues we filed on Google's tracker fixed upstream (PR #6451, PR #6452, PR #6656)

10

live API-validation findings confirmed by ESBMC counterexamples and reproduction; seven filed upstream

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

Three of the seven issues we filed 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. A third, PR #6656 ("Reject milestone zero in ChannelsAPI"), followed on 2026-07-30, resolving Finding C: ?start=0 and ?end=0 now abort with HTTP 400 instead of returning null milestone dates with HTTP 200. Each merged fix is the one we proposed in the issue.

Ten live findings in total; seven filed as upstream issues. We opened seven issues on the chromium-dashboard tracker: #6441, #6442, #6443, #6447, #6464, #6468 and #6469. Three are the ones fixed above. One, ?num=0 silently returning an empty page (#6442), the maintainer closed as benign. Three remain open: a missing feature_changes key raising a KeyError (#6464), an unknown commentId raising an AttributeError (#6468), and an unexpected JSON key raising a TypeError (#6469) — each an HTTP 500 where a 4xx is intended. The remaining three findings (?mstone=0 and metricsdata ?num=0 silent acceptance, and a malformed stage_type POST) are carried as reproducible drafts. 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, PR #6452 and PR #6656 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

  1. lucasccordeiro/chromium-dashboard-esbmc, public PoC repository (harness, witnesses, tiered targets, findings report). github.com/lucasccordeiro/chromium-dashboard-esbmc
  2. 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
  3. 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
  4. GoogleChrome/chromium-dashboard PR #6656, "Reject milestone zero in ChannelsAPI" (merged 2026-07-30); fixes Finding C. github.com/GoogleChrome/chromium-dashboard/pull/6656
  5. GoogleChrome/chromium-dashboard issues #6464, #6468 and #6469, further API-validation findings filed upstream and still open; #6442 was filed and closed by the maintainer as benign. github.com/GoogleChrome/chromium-dashboard/issues/6464
  6. 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 co-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 three fixes merged in PR #6451, PR #6452 and PR #6656, is reproducible from the public repository.

Back to vLLM Discuss your project