Many people assume that Rust’s memory safety automatically makes software secure and correct. Yet recent examples like sudo-rs and TARmageddon, both written in Rust, show this assumption is misleading: even memory-safe software can have logic flaws, privilege errors, or boundary handling bugs.

Adam Zabrocki, in his DEF CON 30 talk, emphasizes that SPARK Ada not only enforces memory safety but also lets developers focus on deeper, more sophisticated security issues. As he notes:

• “Memory Safety does NOT include: Logical bugs, Error handling, Race conditions…”

• “Formally verified software has much higher quality thanks to SPARK enforcements… Most of the bugs which we saw require deep knowledge… architecture problems, design bugs, etc.”

He also points out that the use of SPARK allowed them to spend more time investigating these sophisticated bugs, rather than worrying about trivial memory errors.

While memory-safe features prevent many common issues, SPARK goes further by mathematically guaranteeing correctness and allowing teams to focus on design and architecture level security challenges.

Key takeaway: SPARK provides a level of assurance and error prevention that memory safety alone cannot deliver.

Here is a link to Adam Zabrocki’s DEF CON 30 presentation: https://youtu.be/TcIaZ9LW1WE

(Note: I used ChatGPT to help organize and articulate these insights.)