CVE 2019-5827

4 minute read

Published:

In this blog, we discuss a high-severity vulnerability in Google Chrome that was found by extending the static analysis techniques with symbolic execution.

Discovered Vulnerability: CVE 2019-5827

Attack Vector: Integer overflow in SQLite3 via WebSQL in Google Chrome allowed a remote attacker to potentially exploit heap corruption via a crafted HTML page.

Score/Severity: <h3 style="color:#ff0000">8.8 HIGH</h3>

Summary:

Finding a vulnerable piece of code in a browser is quite difficult. Because the quality of code is relatively better and it is also rigorously tested using the automated analysis tools. Consider an example of Google Chrome browser whose code-base is tested using the ClusterFuzz supported with Clang sanitizers running over +25000 machines.

Both Chrome and Firefox also rely on static analysis to safe-guard against exploitable bugs and also run bug-bounty programs. For example, Firefox is using Cover-scanner since Feb. 2006 that has helped to find hundred of bugs. Unfortunately, these current static analysis techniques fail to find any high-security bug in Firefox since 2014. So does it mean the browser code is bug-free? – Obviously, the answer is NO. The fact is that better code practices and rigorous testing has made it difficult to find one.

Here, we go over a high-severity bug in Google Chrome code that was found using a tool that combines static analysis with symbolic execution to find such bugs in large scale code bases. I build a small example to show how symbolic encoding can help to find and fix such bugs.

Fig 1: The code snippet is retrieved from the repostiory old commit

In Fig 1 we can see the actual vulnerable code that caused CVE 2019-5827. We can see on line 162299 a memory is allocated using malloc. Then on the line 162317 the allocated memory is initialized with zero using memset. Both lines of code share two parameters, one is the assigned memory reference a and input argument nStat. A static analyzer can simply pick on these assignments in a large code base. But it is unable to reason about finding a unique value for nStat that can cause the integers to wrap around and thus triggers the integer overflow leading to a write outside the allocated memory.

We can use a symbolic execution to find a concrete value for nStat using the condition:

memset(a, 0, sizeof(u32)*(nStart) \> malloc(a, 0, sizeof(u32 + 10)*(nStart)

The value returned by the solver should trigger the overflow bug. Lets demonstrate it using an example code.

.

Fig 2: A simple code snippet that share the same vulnerable code as sqlite3.c

We write an example code (Fig 2) that shares the same vulnerable code as the one shown in the original sqllite3.c, see Fig 1. Both static analysis and fuzzing will not help us find a concrete value that triggers an overflow. For finding a value for nStat that triggers this bug we resort to a decision procedure (i.e. an SMT Solver). But this requires us to encode the problem in SMTLib, a language that is accepted by an SMT solver.

Fig 3: An SMTL problem encoding and CVC4 found a highlighted solution

The encoding in Fig 3 is a simple constraint problem encoding asking the solver to 'Find a value for nStart that makes this condition true: memset(a, 0, sizeof(u32)*(nStart) \> malloc(a, 0, sizeof(u32 + 10)*(nStart). Less than a second an SMT solver CVC4 will suggest a value for nStat = 2123844539. Let us confirm that this value does trigger the bug in the example code shown in Fig 2.

Fig 4: Running example using value suggested by SMT Solver

We can see in Fig 2 that when we run the vulnerable code shown in the Figure 2 with the value (2123844539) suggested by CVC4 solver the overflow bug is triggered.

Reference:

[1] Barrett, Clark, Aaron Stump, and Cesare Tinelli. "The smt-lib standard: Version 2.0." Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England). Vol. 13. 2010.

[2] Barrett, Clark, et al. "Cvc4." International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2011.

[3] Brown, Fraser, Deian Stefan, and Dawson Engler. "Sys: a static/symbolic tool for finding good bugs in good (browser) code." 29th {USENIX} Security Symposium ({USENIX} Security 20). 2020.