Verification of the IBOS Browser Security Properties in Reachability Logic

Stephen Skeirik, José Meseguer, Camilo Rocha

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

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.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
EditorsSantiago Escobar, Narciso Martí-Oliet
PublisherSpringer Science and Business Media Deutschland GmbH
Pages176-196
Number of pages21
ISBN (Print)9783030635947
DOIs
StatePublished - 2020
Event13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020 - Virtual, Online
Duration: Oct 20 2020Oct 22 2020

Publication series

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

Conference

Conference13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
CityVirtual, Online
Period10/20/2010/22/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Verification of the IBOS Browser Security Properties in Reachability Logic'. Together they form a unique fingerprint.

Cite this