TY - GEN
T1 - Verification of the IBOS Browser Security Properties in Reachability Logic
AU - Skeirik, Stephen
AU - Meseguer, José
AU - Rocha, Camilo
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85099061790&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-63595-4_10
DO - 10.1007/978-3-030-63595-4_10
M3 - Conference contribution
AN - SCOPUS:85099061790
SN - 9783030635947
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 176
EP - 196
BT - Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
A2 - Escobar, Santiago
A2 - Martí-Oliet, Narciso
PB - Springer Science and Business Media Deutschland GmbH
T2 - 13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
Y2 - 20 October 2020 through 22 October 2020
ER -