Why Riverside Research Employs Formal Methods: It’s an Insurance Policy for Your Technology
Author(s): Tara Clapper, Carl Nerup
When we write code to foster new ideas or develop mission-specific technologies, we advance possibilities in the defense intelligence space. Creating or adjusting code to move a project forward or increase its security is a noble goal, but one you shouldn’t attempt without the application of formal methods.
Envision formal methods as an insurance policy. You wouldn’t buy a house or a car without insurance, so wouldn’t it make sense to insure your software in the same way? With the application of formal methods (FM), you are essentially insuring your software, because formal methods ensure that the code is more resistant to hackers.
What Are Formal Methods in Software Design?
Formal methods are mathematical means of ensuring your code works before you even deploy it, allowing you to adjust and iterate prior to more expansive and expensive application and testing. Formal methods are especially useful in critical areas, such as:
- Secure networks and communications
- Armament management and defense platforms
- Satellite systems and software
- Intelligence, surveillance, and reconnaissance (ISR) systems and data collection methods
- Cryptographic protocols and cybersecurity defense
- AI analysis and decision support
The risks are often more complex than a simple hack. Without safeguarding and futureproofing your code with formal methods, unauthorized users can enter a system and take control of it. This has already happened with commercially available passenger vehicles. Imagine if a hacker took control of a satellite, space shuttle, tank, fighter jet, or armed aircraft carrier.
Not only do formal methods increase safety and security for the warfighter and covert operations, they also reduce general risk when connected systems and interoperability come into play.
Aside from protecting systems from information hacks, a hacked vehicle demonstrates the level of safety that hackers can compromise by getting into systems with software deployed without using formal methods.
How Riverside Research Employs Formal Methods in Mission-Specific Software
Riverside Research employs formal methods in multiple software domains, including parsers, cryptography, and compilers. To design secure cryptographic protocols, for example, teams use techniques derived from Universal Composability (UC), building larger cryptographic systems from secure composable pieces.
Specifically, Riverside Research adds value using formal methods by hardening programs against novel adversaries and threat models even before software is deployed, which is increasingly important as adversaries’ cyber attacks become more automated, self-evolving, and fast-acting.
The Future of Formal Methods in Coding Workflows
Formal methods are increasingly popular and necessary when it comes to coding workflows, such as Continuous Integration/Continuous Deployment (CICD). Imagine if your CICD pipeline could check proofs on every merge request, ensuring that code updates violating your specs never deploy to production. In the long run, protecting secure information means investing in formal methods is worth it.
Invest in a formal methods “insurance policy” and make sure your code is much harder to exploit. Reach out to Riverside Research to explore a collaboration.
Featured Riverside Research Author(s)
Tara Clapper
Tara Clapper is a marketing strategist and content creator at Riverside Research. Her professional background includes technical writing, social media management, publishing, marketing, editorial duties, analog game design, prompt engineering, and content management in govcon, academic, and private sector spaces. Tara helps tell the Riverside Research story by interviewing SMEs for blogs, press releases, and social media channels. Tara holds a Bachelor of the Arts in English from McDaniel College.
LinkedIN
Carl Nerup
Carl Nerup is responsible for Business Development at Riverside Research Institute, including strategic initiatives, partnerships, and alliances. A communications industry veteran, he brings a wealth of knowledge to the leadership team with demonstrated successes in cyber security, embedded systems, mobile/wireless, and new product development.
Prior to Riverside Research’s acquisition of Cog Systems, Carl served as its founder and CEO. He previously worked as the Global Vice President for Samsung where he had responsibility for the secure mobility business. His background also includes strategic development support at General Dynamics and Vice President, Strategic Business Development and Venture & Equity Portfolio Management, at AT&T.
Carl attended the United States Naval Academy and holds a Bachelor of Science from Seattle University. He also received a degree in Data Communication from the University of Washington.
LinkedIN
The above listed authors are current or former employees of Riverside Research. Authors affiliated with other institutions are listed on the full paper. It is the responsibility of the author to list material disclosures in each paper, where applicable – they are not listed here. This academic papers directory is published in accordance with federal guidance to make public and available academic research funded by the federal government.