Tuesday, September 27, 2016

[ptzvyvue] Proven media decoders

It would be nice if a web browser handled every possible media type under the sun; however, this increases the work required for the maintainers, and increases the attack surface of security vulnerabilities for malformed images.  (Ostensibly, these were the reasons given by Mozilla for removing support for MNG; there was probably political component of wanting kill off image formats they did not like.)

For security vulnerabilities, one could add back any media decoder formally proven free of security defects.  They could also have proven resource usage (memory, CPU) characteristics.  Less ambitiously, they could be run in a runtime sandbox that blocks faulty decoders from doing harm as well as enforce constraints of memory and CPU usage.

Continuing along the formal path, the decoder could be proven to correctly decode a specification of an image format (or other media format), at which point the user can download and substitute any other implementation which also is proven follows the spec.  This could provide a mechanism for additional media formats to be introduced aside the browser: an image gives its type, implicitly or explicitly a specification of how it is to be decoded, and the user (user agent) goes out and finds a decoder that is proven to meet the spec (as well as other guarantees).  There remains (among other things) the challenge of a bug-free specification.

No comments :