IBOS 浏览器安全性质在可达性逻辑中的验证
计算机科学中的逻辑
2020-05-26 v1 密码学与安全
形式语言与自动机理论
摘要
本文给出了伊利诺伊浏览器操作系统（IBOS）的重写逻辑规约，并在可达性逻辑中定义了若干安全性质，包括同源策略（SOP）。文中展示了如何使用我们基于构造子的可达性逻辑定理证明器对这些性质进行演绎验证。本文还强调了证明中所使用的推理技术，以及对于扩大验证规模并完成验证工作至关重要的三条模块化原则。
引用
@article{arxiv.2005.12232,
title = {Verification of the IBOS Browser Security Properties in Reachability Logic},
author = {Stephen Skeirik and José Meseguer and Camilo Rocha},
journal= {arXiv preprint arXiv:2005.12232},
year = {2020}
}