3 ms·
You can use a theorem prover like Coq to generate software that proves an image parser correct.
by MichaelBurge 10y ago
You can use a theorem prover like Coq to generate software that proves an image parser correct.
- Silhouette 10y agoExistence proof of a 100% safe image parser built using a formal theorem prover, please.
- Dylan16807 10y agoFor an image parser all you really need is to use a language without buffer overflows.
- Silhouette 10y agoThere are other potential attack vectors than buffer overflows, though that seems the most likely source of vulnerabilities if you're going to limit images to JPG or PNG. Of course now you're not only prohibiting third party resources except images, you're even prohibiting modern image formats like SVG, which is a little ironic since SVG-based ads might be smaller and/or look cleaner than equivalent bitmaps.