Current web browsers are complex, have enormous trusted computing
bases, and provide attackers with easy access to computer
systems. This makes web browser security a difficult issue that
increases in importance as more and more applications move to the
web. Our approach for this challenge is to design and build a
correct-by-construction web browser, called IBOS, that consists of
multiple concurrent components, with a small required trusted
computing base. We give a formal specification of the design of this
secure-by-construction web browser in rewriting logic. We use formal
verification of that specification to prove the desired security
properties of the IBOS design, including the address bar correctness
and the same-origin policy.