IBOS: A correct-by-construction modular browser

Ralf Sasse, Samuel T. King, José Meseguer, Shuo Tang

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationFormal Aspects of Component Software - 9th International Symposium, FACS 2012, Revised Selected Papers
Number of pages18
StatePublished - 2013
Event9th International Symposium on Formal Aspects of Component Software, FACS 2012 - Mountain View, CA, United States
Duration: Sep 12 2012Sep 14 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7684 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other9th International Symposium on Formal Aspects of Component Software, FACS 2012
Country/TerritoryUnited States
CityMountain View, CA


  • Browser security
  • rewriting logic
  • same-origin policy

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'IBOS: A correct-by-construction modular browser'. Together they form a unique fingerprint.

Cite this