Finding a billion-user project for Eiffel: How DbC catches the security flaws that Rust misses
Finnian Reilly
Friedrich Dominicus
DBC wird imer noch massiv unterschätzt. (Warum auch immer)
--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/4e728a1c-4efd-40cf-b397-87f334030a0an%40googlegroups.com.
lar...@eiffel.com
Thank you Finnian!
From: eiffel...@googlegroups.com <eiffel...@googlegroups.com> On Behalf Of Finnian Reilly
Sent: Friday, May 22, 2026 1:36 PM
To: Eiffel Users <eiffel...@googlegroups.com>
Subject: [eiffel-users] Finding a billion-user project for Eiffel: How DbC catches the security flaws that Rust misses
Finding a billion-user project for Eiffel
How DbC catches the security flaws that Rust misses
Summary of article on eiffel.org
The industry is currently celebrating Rust as a breakthrough in software safety. But Eiffel had a more complete answer to software correctness before Rust's creator was born. This essay argues that the moment has arrived for the Eiffel community to demonstrate that publicly — with a specific project, a real deployment strategy, and a compelling security argument.
Ulrich Windl
I have studied the latest Eiffel compiler, nor did I try the latest Rust compiler, but from what I saw in the past was that the Rust compiler was quite good in static analysis during compilation (without the user having to add additional assertions), while Eiffel may detect violated assertions during runtime. So somehow it seems that Rust uses the more advanced compiler technology. However, I'm aware that many errors the Rust compiler complains about cannot happen in Eiffel. This is another performance against comfort issue.
I'd advise the Eiffel community to look at the good things in Rust, rather than bashing at it with a "we are so much better". However, the syntax of Rust is really ugly, maybe even uglier than that of C.
Kind regards,
Ulrich
22.05.2026 13:36:14 Finnian Reilly <frei...@gmail.com>:
> Finding a billion-user project for Eiffel
> How DbC catches the security flaws that Rust misses
>
> https://www.eiffel.org/blog/Finnian%20Reilly/2026/05/finding-billion-user-project-eiffel-how-dbc-catches-security-flaws-rust-misses
> --
> You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
Finnian Reilly
> I'd advise the Eiffel community to look at the good things in Rust, rather than bashing at it with a "we are so much better". However, the syntax of Rust is really ugly, maybe even uglier than that of C.
what Rust does well. The specific claim is narrower: that Design by
Contract catches logic errors like the sudo-rs CVEs of 2025, which
Rust's static analysis cannot address because they're not memory errors.
--
SmartDevelopersUseUnderScoresInTheirIdentifiersBecause_it_is_much_easier_to_read
Eric Bezault
> I have studied the latest Eiffel compiler, nor did I try the latest Rust compiler, but from what I saw in the past was that the Rust compiler was quite good in static analysis during compilation (without the user having to add additional assertions), while Eiffel may detect violated assertions during runtime.
during compilation? This is the promise of Autoproof.
After many years as a research project, Autoproof is
already able to detect many kinds of assertion violations.
There is a (several year old) prototype/demo available
online:
http://comcom.csail.mit.edu/comcom/#AutoProof
Can you find why class ACCOUNT is broken in this example?
Just fix it and click on Run again...
Having such tool in production would be a killer in
the era of AI generated code. The assertions would be
the specification provided to the AI, and Autoproof
would automatically verify that the generated code
satisfies these assertions.
If there are some companies interested in such technology
and ready to invest money to support this work, this
sponsorship would allow me to join the team and help turn
this research project into a mature production tool
integrated into the Eiffel ecosystem. Please contact me
or Eiffel Software for further discussion.
--
Eric Bezault <er...@gobosoft.com>
Eiffel expert - available for freelance work
https://www.gobosoft.com
Ian Joyner
"I'd advise the Eiffel community to look at the good things in Rust, rather than bashing at it with a "we are so much better”.”
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/2a3ceb58-ba70-41cd-acec-362529266c66%40gmail.com.
javier...@gmail.com
With AutoProof (Code Verifier ), we move bug detection from `runtime exceptions --> compile-time verification.`
Spec + DbC
--> Poof Pass?
Yes --> [Execute]
No --> Violation details back to LLM | Review the Spec
See a related complementary approach about formal verification to AI agent workflows https://dl.acm.org/doi/epdf/10.1145/3777544 about
The article Guardian of Agents is a higher level, for Agents' Orchestrations, a kind of Workflow Verifier.
Anders Persson
--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/0d115ad6-e885-4954-be86-be995ed7e7e1n%40googlegroups.com.
Ian Joyner
On 22 May 2026, at 21:36, Finnian Reilly <frei...@gmail.com> wrote:
Finding a billion-user project for EiffelHow DbC catches the security flaws that Rust missesSummary of article on eiffel.orgThe industry is currently celebrating Rust as a breakthrough in software safety. But Eiffel had a more complete answer to software correctness before Rust's creator was born. This essay argues that the moment has arrived for the Eiffel community to demonstrate that publicly — with a specific project, a real deployment strategy, and a compelling security argument.
<Finding a billion-user project for Eiffel How DbC catches the security flaws that Rust misses.png>
--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/4e728a1c-4efd-40cf-b397-87f334030a0an%40googlegroups.com.
Finnian Reilly
Two New Sections 13 and 14
For completeness I have inserted two new sections into the eiffel.org essay. You can read them below.
regards
Finnian
13. Eiffel's static verification ecosystem: AutoTest and AutoProof
AutoTest is a contract-driven automated test generation tool integrated into EiffelStudio. Rather than requiring developers to write test cases manually, AutoTest reads existing DbC contracts and generates test inputs automatically — using random and systematic strategies to find inputs that satisfy preconditions, executing routines, and checking whether postconditions and invariants hold. A contract violation becomes an automatically discovered bug without a human having written the test that found it. For xpact, AutoTest would automatically generate both valid and malformed XML inputs, exercising the parser's contract boundaries continuously as development proceeds. The contracts serve double duty: specification and test oracle simultaneously.
AutoProof goes further still — it attempts to prove Eiffel contracts correct at compile time using SMT solvers (Satisfiability Modulo Theories), most notably Microsoft Research's Z3 engine. Rather than finding violations empirically, AutoProof seeks mathematical proof that violations are impossible for all inputs. If a proof succeeds, the guarantee is not "we tested this extensively" but "this is provably correct." AutoProof translates Eiffel contracts into logical propositions and attempts to determine their truth mathematically. A successful proof eliminates an entire class of bug not just for tested inputs but for every possible input. AutoProof currently remains a research prototype — scaling to production codebases of arbitrary complexity is an unsolved problem, and many correct programs cannot yet be automatically proven within practical time bounds. However xpact's bounded, specification-driven domain — a streaming parser implementing a formal grammar with well-defined invariants derived directly from the XML specification — represents close to an ideal case for AutoProof. The possibility of mathematically proving xpact's core parsing contracts correct is realistic in a way that it would not be for a large general-purpose application.
The layered correctness picture for xpact is therefore:
- Void safety — static, always on, eliminates null dereference at compile time regardless of contract mode
- DbC contracts — verified against the complete libexpat test suite including all CVE regression tests, with full contract checking enabled
- AutoTest — automatic test generation driven by contracts, continuously exercising contract boundaries without manual test authorship
- AutoProof — mathematical proof of correctness for provable components, eliminating entire bug classes for all possible inputs
- Fuzzing — adversarial input coverage via OSS-Fuzz for the unprovable remainder
No other language or toolchain currently offers this combination for a security-critical parser. Rust eliminates memory corruption. Eiffel eliminates memory corruption, proves logic correctness, generates tests from specifications, and offers a path to mathematical verification — all from the same codebase, with the same annotations serving every layer.
14. A living contract suite: learning from the entire XML parser ecosystem
One of the less obvious advantages of xpact's contract-driven architecture is that it can learn continuously from security research happening across the entire XML parsing ecosystem — not just libexpat's CVE history.
Every XML parser CVE ever published represents a logic error that a correctly written contract would have prevented. libexpat, libxml2, Xerces-C++, MSXML, RapidXML — each has its own CVE history, and many of those vulnerabilities share common root causes: unbounded recursion depth, unconstrained entity expansion ratios, integer overflow on length calculations, negative length acceptance, algorithmic complexity attacks from crafted input structures. These are not libexpat-specific failures. They are recurring patterns in XML parser implementations across languages, decades, and organisations.
This collective CVE history is, in effect, a collaboratively written specification of what an XML parser must constrain — contributed inadvertently by security researchers and attackers worldwide. xpact can treat it as such.
The AI-assisted contract derivation workflow
Claude and similar AI tools are well suited to systematic CVE analysis. The workflow is straightforward:
- Fetch CVE descriptions and root cause analyses for all major XML parsers
- Categorise each CVE by the class of constraint that was missing — recursion depth, expansion ratio, buffer length, integer range, complexity bound
- Map each category to a specific Eiffel precondition or invariant
- Identify which constraints xpact already expresses as contracts and which are absent
- Suggest specific Eiffel contract annotations for the gaps
This turns the entire XML parser CVE database into a continuously updated contract specification. As new CVEs are published for any XML parser, the same analysis applies — a new vulnerability anywhere in the ecosystem becomes a contract suggestion for xpact within days of disclosure rather than years after exploitation.
The inversion worth noting
This is a remarkable inversion of the usual security dynamic. Normally attackers discover vulnerabilities and defenders react. In xpact's model, every vulnerability discovered anywhere in the XML parsing ecosystem — past, present, and future — automatically strengthens xpact's contract suite. Attackers inadvertently contribute to xpact's correctness story. The CVE database becomes a collaborative specification written by the world's security researchers.
The other significant XML parsers
libexpat is the most widely embedded XML parser but the CVE landscape is broader. libxml2 — used by GNOME, Python's lxml, PHP, and many others — has an even longer CVE history and supports XPath, XPointer, and full validation, making it a natural Phase 2 target once xpact establishes its libexpat-compatible core. Xerces-C++ (Apache) has a significant enterprise deployment footprint with its own history of denial-of-service vulnerabilities from crafted inputs. RapidXML and pugixml are widely used in game development and embedded systems — less security scrutiny means their CVE surface may be underreported rather than absent.
The living contract suite
Combined with AutoTest and OSS-Fuzz continuous fuzzing, xpact's contract suite would be updated from three complementary sources: systematic analysis of historical CVEs across all XML parsers, new CVEs as they are published, and AutoTest-discovered violations during active development. This is a specification that grows more complete over time automatically — the opposite of how most security-critical libraries evolve, where specifications are static and vulnerabilities accumulate. xpact's contracts do not just reflect what we know today. They are designed to incorporate what the security community will discover tomorrow.
-- SmartDevelopersUseUnderScoresInTheirIdentifiersBecause_it_is_much_easier_to_read
Finnian Reilly
noticed the loop invariants already in place. That is exactly the spirit
the essay was hoping to inspire. Looking forward to watching xpact take
shape.
Vänligen
Finnian
--
SmartDevelopersUseUnderScoresInTheirIdentifiersBecause_it_is_much_easier_to_read
Finnian Reilly
thanks for taking the time. You're right that the essay addresses only one layer of a multi-layer problem. Platform security is the foundation everything else rests on. But if attackers will always find the weakest layer, then making each layer as fortified as possible is the only rational response. Within the application layer — where most CVEs that affect end users actually originate — DbC addresses a class of logic errors that platform security cannot prevent and that Rust's model doesn't reach. The sudo-rs authentication bypass was a logic error that would have run correctly on even the most secure platform. That's the specific gap the essay is addressing. The two concerns are complementary — platform security and application-layer correctness both matter. xpact addresses the latter
Regards
Finnian Reilly
New section added: xpact vs expat — bridging the performance gap
A new section has been added to the eiffel.org essay addressing the performance question that any serious xpact proposal must answer: can an Eiffel XML parser compete with a highly optimised C library on raw throughput?
The section introduces C_STRING_8, a lightweight proof-of-concept class that wraps C-allocated memory directly via MANAGED_POINTER inheritance, with string operations delegated to memcmp and memcpy. The benchmarks comparing it against STRING_8 (SPECIAL-backed) show some striking results:
- starts_with — C buffer 59.7% faster
- occurrences — C buffer 22.3% faster
- CSV parsing — C buffer 20.0% faster
The starts_with result is the most significant for xpact — token prefix recognition is the dominant operation in XML parsing, and a 59.7% advantage on that operation compounds substantially across a full document parse.
Beyond raw speed, the section discusses a zero-copy parse architecture using shared substrings — every token the parser recognises becomes a lightweight window into the original input buffer with no character copying and no additional heap allocation. For large documents this halves the GC object count per token compared to STRING_8, since C_STRING_8 requires only one heap object per string rather than the two that STRING_8 requires (instance + SPECIAL [CHARACTER_8]).
The full section including Eiffel source listings is at:
Benchmark source code + C_STRING_8 attached
Finnian
Finnian Reilly
Re: xpact vs expat — bridging the performance gap
Benchmark source code + C_STRING_8 attached
Ulrich Windl
Contracts don't make codes correct; they just flag bad code.
Ulrich
28.05.2026 15:34:14 Finnian Reilly <fin...@eiffel-loop.com>:
Finnian Reilly
XML name interning: a zero-copy, cache-efficient strategy for xpact callbacks
New section added to the "Billion User" essay — 1,700 words
This new section addresses one of the subtler engineering challenges in making xpact a genuine libexpat drop-in replacement — satisfying the null-termination contract of the C callback API without abandoning the zero-copy parse architecture.
The solution turns out to be more elegant than expected, eliminating the need for GC pinning entirely through a new class C_NULLED_STRING_8 that allocates directly in C memory. The section covers:
- The intern table — mapping non-null-terminated parse tokens to cached null-terminated C strings
- C_NULLED_STRING_8 — why C-allocated memory sidesteps the GC pinning problem entirely
- Why binary search rather than a hash table — the case for a sorted arrayed map list for typical XML vocabularies
- Bucketing by first character — scaling gracefully to larger vocabularies
- Linear or binary search chosen automatically — with a tunable threshold constant of 10
- The unit test — proving identity rather than equality, with 12 'a' words exercising the binary search threshold
- A C programmer's perspective — why the same architecture is hazardous to maintain in C but self-verifying in Eiffel
- What this means for xpact — the complete Phase 2 performance roadmap
All classes — C_NULLED_STRING_8, C_NULLED_STRING_8_NAME_CACHE, and the unit test — are implemented and tested in Eiffel-Loop under the MIT licence, ready for Anders to draw on when Phase 2 begins.
Finnian
Finnian Reilly
Eric Bezault
Is the mapping C_STRING_8 -> C_NULLED_STRING_8 only needed for
element and attribute names? The advantages that you describe
in using C_NULLED_STRING_8 are based on the small size of the
vocabulary typically used in XML files, namely element and
attribute names. But what about attribute values, user text
between <foo> and </foo>, comments, etc. They are often unique
and can sometimes be large and/or numerous. Do these strings
also need to be mapped from C_STRING_8 to C_NULLED_STRING_8?
--
Eric Bezault <er...@gobosoft.com>
Eiffel expert - available for freelance work
https://www.gobosoft.com
> *XML name interning: a zero-copy, cache-efficient strategy for xpact
> callbacks <https://www.eiffel.org/blog/Finnian%20Reilly/2026/05/finding-
> billion-user-project-eiffel-how-dbc-catches-security-flaws-rust-
> misses#XML_name_interning:_a_zero-copy,_cache-
> efficient_strategy_for_xpact_callbacks>*
>
> *New section added to the "Billion User" essay — 1,700 words*
> This new section addresses one of the subtler engineering challenges in
> making xpact a genuine libexpat drop-in replacement — satisfying the
> null-termination contract of the C callback API without abandoning the
> zero-copy parse architecture.
>
> The solution turns out to be more elegant than expected, eliminating the
> need for GC pinning entirely through a new class C_NULLED_STRING_8 that
> allocates directly in C memory. The section covers:
>
> cached null-terminated C strings
> * *C_NULLED_STRING_8* — why C-allocated memory sidesteps the GC
> pinning problem entirely
> * *Why binary search rather than a hash table* — the case for a sorted
> vocabularies
> * *Linear or binary search chosen automatically* — with a tunable
> threshold constant of 10
> * *The unit test* — proving identity rather than equality, with 12 'a'
> All classes — C_NULLED_STRING_8, C_NULLED_STRING_8_NAME_CACHE, and the
> unit test — are implemented and tested in Eiffel-Loop under the MIT
> licence, ready for Anders to draw on when Phase 2 begins.
>
> https://www.eiffel.org/blog/Finnian%20Reilly/2026/05/finding-billion-
> user-project-eiffel-how-dbc-catches-security-flaws-rust-
> misses#XML_name_interning:_a_zero-copy,_cache-
> Finnian%20Reilly/2026/05/finding-billion-user-project-eiffel-how-dbc-
> catches-security-flaws-rust-misses#XML_name_interning:_a_zero-
> copy,_cache-efficient_strategy_for_xpact_callbacks>
> Finnian
>
>
>
> On Friday, 22 May 2026 at 12:36:15 UTC+1 Finnian Reilly wrote:
>
> Finding a billion-user project for Eiffel
> How DbC catches the security flaws that Rust misses
>
> You received this message because you are subscribed to the Google
> Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send
> users+un...@googlegroups.com>.
> groups.google.com/d/msgid/eiffel-users/
> a6106d43-89ca-4c11-9434-3af8bd9df075n%40googlegroups.com?
> utm_medium=email&utm_source=footer>.
Finnian Reilly
Callback string types and the appropriate Eiffel class
Not all callback strings benefit equally from the name cache. The following table maps each libexpat callback type to its string representation, the appropriate Eiffel class, and whether caching is beneficial:
Finnian Reilly
Finnian Reilly
Hi Friedrich,
your VBA experience is one of the most compelling endorsements of DbC I have seen — not because VBA is a great language for it, but precisely because it isn't. You found DbC valuable enough to implement it by hand in a language with no native support, which says everything about the practical worth of the idea.
Your point b) is particularly insightful and deserves more attention than it usually gets. Conventional quality tools — static analysers, code review, test coverage — all struggle to scale as codebases grow. DbC scales naturally because the contracts live in the code itself rather than in external tooling. A precondition on a routine is just as enforceable in a million-line codebase as in a hundred-line one.
This is exactly why xpact — the Eiffel XML parser proposed in the essay — uses DbC not just as a debugging aid but as the primary correctness argument. The contracts derived from the XML specification scale with the parser's complexity by construction.
In Eiffel of course you don't have to implement any of this by hand. It is native to the language, supported by the IDE, enforced automatically during testing, and statically verifiable via AutoProof. Everything you built in VBA by discipline is just part of the syntax.
FinnianUlrich Windl
A somewhat random comment: Some years ago (it was the time of the 200Mhz Pentium Pro) I wrote a parser for MIME E-Mail messages in order to scan for malware. Using the absolute evil language (C) I had thought how that could be done efficiently, and (considering the small CPU cache) I came to the conclusion that I'll have to avoid copying strings whenever possible and use references to substrings instead (MIME's multi-part messages may be nested just like XML can be, and the content can be encoded). The fortunate part was that the decoded string would always be shorter than the original, so I could replace it "in-place". You can guess memory management was a bit tricky, but it worked well.
When thinking to do something similar for XML, the problem are entity references, a kind of encoding that may be LARGER than the original, to working with zero-copy and substring references won't work.
Also today's CPUs have caches so large that the whole Windows/95 would fit into them and memory bandwidth is probably 100 times as fast.
Still: Can an OO solution be time and space efficient?
(One of my experiences with SGML parsers was that they would need 32MB RAM (that was all I had at that time) to process an 1MB input file. That made me think about the design.)
When processing MIME one could save the message body to a string, then create an array for all the parts the main message defines, copying the parts, and then recursively parse each of the sub-parts for further sub-divisions, eventually applying the decoding into new strings, keeping the garbage collector busy, or having multiple equivalent copies of those parts in memory (or on disk). Obviously that was not what I wanted to do, even if that's the straight forward and clean design...
Regards,
Ulrich