{"id":48204398,"user":"pjc50","time":1779262777,"time_ago":"10 hours ago","type":"comment","content":"

UB based on input can be an exploit vector.","comments":[{"id":48204491,"user":"layer8","time":1779263581,"time_ago":"10 hours ago","type":"comment","content":"

Unvalidated input can always be an exploit vector.","comments":[{"id":48204516,"user":"Ygg2","time":1779263898,"time_ago":"10 hours ago","type":"comment","content":"

Except in C, validation of user input can in itself be an exploit vector.","comments":[{"id":48204692,"user":"layer8","time":1779265487,"time_ago":"9 hours ago","type":"comment","content":"

That’s true in other languages as well. Any programmatic task can end up being an exploit vector.","comments":[{"id":48204874,"user":"pjc50","time":1779267155,"time_ago":"9 hours ago","type":"comment","content":"

No? That's the whole point of formal verification?

You can even kind of retrofit this to C. The classic example is "sel4". You just need a set of proofs that the code doesn't trigger UB. This ends up being much larger and more complicated than the C itself.","comments":[{"id":48206091,"user":"rocketrascal","time":1779276867,"time_ago":"6 hours ago","type":"comment","content":"

You can fail to verify something which you actually wanted to verify (i.e you made a proof of something else instead of the thing that mattered). See WPA2 KRACK as an example.","comments":[],"comments_count":0,"level":4,"url":"item?id=48206091"}],"comments_count":1,"level":3,"url":"item?id=48204874"},{"id":48209120,"user":"Ygg2","time":1779289865,"time_ago":"2 hours ago","type":"comment","content":"

Yeah, but only in C* can those errors end up as more UB.

* terms and limits may apply.","comments":[],"comments_count":0,"level":3,"url":"item?id=48209120"}],"comments_count":3,"level":2,"url":"item?id=48204692"},{"id":48204566,"user":"greybeard69","time":1779264263,"time_ago":"9 hours ago","type":"comment","content":"

Turtles all the way down.","comments":[],"comments_count":0,"level":2,"url":"item?id=48204566"}],"comments_count":5,"level":1,"url":"item?id=48204516"}],"comments_count":6,"level":0,"url":"item?id=48204491"}],"comments_count":7,"url":"item?id=48204398"}

Comment by pjc50