Formal Methods and a Mathematical Proof of Zero Bugs in Code
ISSA Silicon Valley, at the Mountain View Campus of Microsoft
July 18th, 2023
Speaker: Benjamin Monate, CTO & Co-Founder at TrustInSoft
Formal methods play a crucial role in raising the security and safety level of firmware, which is an essential component of modern computing systems. Firmware, being the low-level software responsible for controlling hardware devices, presents unique challenges due to its direct interaction with critical system functionalities. This talk highlights the importance of employing formal methods as a means to enhance the security and safety aspects of firmware development. By providing mathematical rigor and systematic analysis, formal methods enable the detection and prevention of security vulnerabilities, backdoors, and safety hazards. Incorporating formal methods into the firmware development process is crucial for building robust, trustworthy systems that safeguard against cyber threats and ensure user safety.
Learn more at trust-in-soft.com
00:00 - 01:00: Introduction
01:00 - 11:24: Security of firmware with formal methods
11:24 - 14:53: Firmware security: formal verification and security
14:55 - 22:04: Intro to Abstract Interpretation in Software
22:06 - 27:52: Mathematics is not magic
27:53 - 35:13: Abstract Interpretation in Software Verification
35:16 - 36:40: The Future of Software Development
36:40 - 37:42: Q&A
37:42 - 40:27: Secure Software: The Next Step
40:27 - 45:52: What's the barrier to entry for finding bugs in C?
45:52 - 50:13: Code Verification in C and Java
50:13 - 50:40: Conclusion
______________________________________
Discover TrustInSoft Analyzer: https://trust-in-soft.com/trustinsoft...
Book a Demo with one of our experts: https://trust-in-soft.com/contact/
Interested to learn more? 💡
Check out our recent blogs: https://trust-in-soft.com/resources-n...
Download our white papers: https://trust-in-soft.com/resources-n...
Watch previous webinars: https://trust-in-soft.com/resources-n...
Keep in touch with us! 📲
LinkedIn: / trustinsoft
X: https://x.com/TrustInSoft
_____________________________________
TrustInSoft's products reduce cyber risks, lower the cost of designing safety-critical systems, and reduce liabilities. Founded in 2013, the Paris-based company provides software developers, testers, and integrators with TrustInSoft Analyzer, an exhaustive static analysis tool that interprets source code using formal methods to detect all of the most frequent and dangerous families of threats and coding errors before deployment. TrustInSoft also offers professional services and expertise to formally audit safety and security-critical existing software components. For more information, visit https://trust-in-soft.com.