On: All the giant companies used ffmpeg (2020)

[qayxc]

> It's just not humanly possible to get this right in every instance.

That's what theorem provers and model driven development are for.

I wish these tools could be used more. There should also be automated completeness checkers for requirements and specs - a lot of errors, incompatibilities and security issues are the result of ambiguous, contradictory, or incomplete specs and requirements.

[marcan_42 → qayxc]

> That's what theorem provers and model driven development are for.

That's building a safe programming language on top of an unsafe one. At that point you might as well just use a safe programming language.

That won't fix logic errors, but the vast majority of security issues are safety problems, especially in this kind of codebase.

[ellis0n → qayxc]

There is no algorithm in the world for how to check whether a video codec is working correctly or not

[afiori → ellis0n]

The model checking would not check the output but the trace of operations.

It might prove that all bytes of the output were written to at least once, that dereferenced pointers point toward either the input or some other valid structure, and other properties like this.