  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.
