Verification of the IBOS Browser Security Properties in Reachability Logic

TL;DR

This paper develops a formal verification framework for IBOS browser security properties using reachability logic, enabling deductive proofs of policies like SOP with scalable reasoning techniques.

Contribution

It introduces a rewriting logic specification of IBOS and demonstrates how to verify security properties using a novel reachability logic theorem prover.

Findings

Successful formal verification of IBOS security properties

Development of a modular reasoning approach for scalable proofs

Implementation of a reachability logic theorem prover for browser security

Abstract

This paper presents a rewriting logic specification of the Illinois Browser Operating System (IBOS) and defines several security properties, including the same-origin policy (SOP) in reachability logic. It shows how these properties can be deductively verified using our constructor-based reachability logic theorem prover. This paper also highlights the reasoning techniques used in the proof and three modularity principles that have been crucial to scale up and complete the verification effort.