Formal verification of RLBox validators

The renderer process in a Firefox browser depends on numerous third-party libraries to render media – audio, images, video and other content – exposing it to web attacks. The attackers use the vulnerabilities in the third-party library code to trigger browser crashes or even achieve code execution within the browser. To protect the renderer from such vulnerabilities, the RLBox library focuses on hardening the renderer-library boundary by sandboxing a third-party library in its own process and providing a dedicated tainted type system to identify data that interacts with the sandboxed library’s functions. RLBox disallows any computation on the tainted data in the renderer as it could affect the control and/or data flow. For the developer to be able to use the tainted data within the renderer code, they need to eliminate the taint type. To remove the taint RLBox has functions, also known as validation methods, where developers add in checks for the values returned from the library function. This urges the developers to think through all cases thoroughly, specifically the corner cases, which can be very challenging since the unwrapped value might not have immediate apparent consequences but could cause memory violations – out-of-bounds reads or writes –upon later uses. 

In order to spot faulty validators, we propose a formal verification-based approach that will give users additional guidance through counter examples to construct conditions on the return values and enables the user to make informed decisions about their validators. In this work, we use DIVINE, an explicit-state LTL model checker, to formally verify the validators exhaustively. We developed C++ applications that sandbox external libraries using RLBox. We tested the validators written in the application to identify incorrect conditions and provide counterexamples. Overall, our work emphasizes the benefit of employing formal verification to strengthen the validators, which are crucial in the renderer-library boundary hardening.