Security News > 2021 > January > Three ways formal methods can scale for software security

FM tools can determine whether a design has lurking security issues before implementation begins; show that an implementation matches the system design; and prove that the implementation is free of introduced defects such as low-level memory errors.

Current and emerging FM re-imagines the ways FM tools can be practically applied to a broad range of software projects.

Formal methods in principle can verify almost any property about a piece of software, but real tools must trade precision against the scale of the software.

Modern formal methods have solved this dilemma by developing a range of tools appropriate for different scenarios.

Scaling formal methods will be greatly aided by improving awareness of the various tools available and which tools are best for your organization.

Amazon has applied the formal verification tool SAW to aspects of s2n, its TLS library protecting AWS. Middleweight tools include symbolic testing tools such as CBMC and network analysis tools such as Amazon's Tiros tool.

News URL

http://feedproxy.google.com/~r/HelpNetSecurity/~3/7uHeyVZMcLE/