Hardening attack surfaces with formally proven binary format parsers

Re:Hardening attack surfaces with formally proven binary for... by tonmoy on Monday July 04, 2022 @06:35AM (#31975570)

This is not new for MS. Windows 98 and XP would get a lot of BSOD because of third party drivers doing illegal things. MS have been investing heavily in formal verification since early 2000s because of that. My master’s adviser (and many more professors working in formal verification) would get most of their funding from MS. One early successful example I can think of is SLAM[1]

1. https://www.microsoft.com/en-us/research/project/slam/

[ Parent | on HN ]

Re:Hardening attack surfaces with formally proven binary for... by staticassertion on Monday July 04, 2022 @02:12PM (#31980145)

Also, P. https://www.microsoft.com/en-us/research/blog/p-programming-...

> P got its start in Microsoft software development when it was used to ship the USB 3.0 drivers in Windows 8.1 and Windows Phone

[ Parent | on HN ]