At BlackBerry, we know that security is only as strong as its weakest link, so it’s critical to have a comprehensive security strategy. As director of BlackBerry’s Center for High-Assurance Computing Excellence (CHACE), I lead our company’s research into the next generation of security and security assurance.
This blog was written by Andrew Walenstein.
BlackBerry powered by Android includes rapid patching, often in tandem with public disclosure, as a basis of our security incident response. We harden the Android platform and offer our customers the industry’s leading cross-platform Enterprise Mobility Management (EMM) solutions. Security and privacy have been in our DNA since before we invented the smartphone and EMM.
But a comprehensive security strategy also constantly looks for improvements. As an industry, we need to get to a point where products with security flaws never make it into customers’ hands. But, a quick look at the U.S. National Vulnerability Database shows how far we still have to go – over 77,000 security vulnerabilities are publicly documented across nearly every major smartphone, tablet, and PC platform. We’re obviously not going to fix all of these overnight, but we need to start somewhere. Our goal isn’t just to “try hard” to eliminate them; we want to be able to prove that we have eliminated them – completely.
The idea of routinely provable security is actually quite new to the technology industry. Technical innovation is built around rapid development and iteration, with quality and security usually taking a backseat to features and functionality. Security testing is often inconsistent across different products and services, and even when performed properly, can only show the presence of bugs, NOT the absence of bugs. Given these facts, is it any wonder that the cost of cyberattacks is projected to reach $3 trillion in the next five years?
Formal Methods
Formal methods use mathematical logic to describe software and to prove that products, services, and systems are secure (or insecure). NASA uses formal methods to establish the safety and functional properties of avionics systems; Intel uses formal verification to control properties of hardware and firmware; and Microsoft provides a tool for proving properties of device drivers. BlackBerry’s own QNX division builds embedded solutions for safety-critical applications such as cars, medical devices, and even power plants. QNX includes formal methods in its software process for these use cases; it takes special effort and highly trained personnel to apply the existing tools, but the benefits easily outweigh the costs.
BlackBerry is working to extend the reach of formal methods into existing development lifecycles and to raise the bar for formal methods used in the security industry as a whole. We’ve been fortunate to team up with a world leader in the practical application of formal methods: Oxford University’s Systems Verification Group, led by Prof. Daniel Kroening.
Let’s Get Nerdy
The Systems Verification Group seeks innovations in a formal method technique called “model checking.” Suppose you have a piece of software and you want to prove that it’s secure: the first step is to create a mathematical model of what you consider to be the normal behavior of the system. Any behaviors outside of the model are unwanted behaviors, such as system crashes and security breaches. Model checking is a way of automatically proving that there is no way for the hardware or software to behave outside your model. Or finding that there is: that’s a fault that must be fixed before release.
Unfortunately, applying this to real software is not so easy. It takes careful effort by a trained engineer to apply model checking in practice, especially when bringing formal methods to existing code: someone must determine new, formal security checks, add them to the code, add their verification to the builds, and ensure their ongoing maintenance to the lifecycle. Our goal is to reduce the cost of applying model checking to software in real-world situations.
To investigate, we tested this on our very own PRIV by BlackBerry smartphone. We looked at code that had already been assessed by our professional security architects and attacked by our team of internal hackers in a formal Vulnerability Assessment (VA). Could bounded model checking apply to that critical code? Could the tools find the flaws our security professionals had identified for fixing? Could we find any they missed? Yes, yes, and yes.
We specifically looked for buffer overruns and integer overflows — the kinds of flaws that were to blame for the recent Stagefright vulnerabilities that affected over a billion smartphones. What we found was excellent code with very few potential security flaws. We found integer overflows that our security experts also flagged. (Remember, we were checking the same development version the VA looked at.) We also found a potential integer overflow that was not flagged by the vulnerability analysis, but upon careful inspection we discovered it was not exploitable. So while that was a false lead, overall it showed that automated formal methods let us find the “last few bugs,” which sometimes lurk unnoticed for years.
A Future Without Vulnerabilities
When we as individuals buy electronic devices and use online services, we assume that they’re secure and that they will protect our private information. But all too often, these assumptions turn out to be wrong, as highlighted by the constant news stories on major cyberattacks and data breaches. The root of the problem is the typical industry approach to security: build products, ship them, and hope they don’t get hacked.
At BlackBerry, we’re working day and night to turn this security model on its head. Rapid patching is critical to product security, but the reactive approach gives the attacker the opening move. Formal methods have the potential to proactively improve security design standards and certifications, giving us the ability to prove that products and services are secure – including the obscure details that even the experts sometimes overlook. With the cybersecurity battle raging on, formal methods can change the battlefield over the long term and give us the best possible chance to win the war.