Verification of the IBOS Browser Security Properties in Reachability Logic

May 25, 2020 · The Ethereal · 🏛 Workshop on Rewriting Logic and Its Applications

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Stephen Skeirik, José Meseguer, Camilo Rocha arXiv ID 2005.12232 Category cs.LO: Logic in CS Cross-listed cs.CR, cs.FL Citations 3 Venue Workshop on Rewriting Logic and Its Applications Last Checked 5 months ago
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.
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS