Interactive Theorem Proving
Interactive Theorem Proving
复制标题
交互式定理证明
DOI：
10.1007/978-3-319-43144-4_6
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Bauereiß T
中科院分区：
文献类型：
--
作者：
Bauereiß T
本文描述了我们对现实系统的信息流安全进行形式化验证的进展。我们介绍了CoSMed，一个经过验证的文件保密的社交媒体平台。系统的内核在证明助手Isabelle/HOL中实现并验证。为了验证，我们采用了之前为会议系统coon引入的有界可演绎性（BD）安全框架。CoSMed是该框架中的第二个主要案例研究。对于CoSMed，以前的BD Security实例所特有的解密边界和触发器的静态拓扑必须让位于作为边界一部分的触发器的动态集成。我们还表明，从理论的角度来看，从BD安全性的概念中删除触发器并不限制其表达性。
This paper describes progress with our agenda of formal verification of information flow security for realistic systems. We present CoSMed, a social media platform with verified document confidentiality. The system’s kernel is implemented and verified in the proof assistant Isabelle/HOL. For verification, we employ the framework ofBounded-Deducibility (BD) Security, previously introduced for the conference system CoCon. CoSMed is a second major case study in this framework. For CoSMed, the static topology of declassification bounds and triggers that characterized previous instances of BD Security has to give way to a dynamic integration of the triggers as part of the bounds. We also show that, from a theoretical viewpoint, the removal of triggers from the notion of BD Security does not restrict its expressiveness.
登录
查看更多内容
影响因子：
1.1
作者：
Maric, Filip
通讯作者：
Maric, Filip
流水线机器的正确性
DOI：
--
发表时间：
2000
期刊：
Formal Methods in Computer-Aided Design
影响因子：
--
作者：
P. Manolios
通讯作者：
P. Manolios
Z3 -QCD 和持久同源性
DOI：
--
发表时间：
2022
期刊：
Annual report 2021 (2021 Highlights), RCNP, Osaka University
影响因子：
--
作者：
Hiroaki Kouno;Kashiwa Kouji、Hirakida Takehiro
通讯作者：
Kashiwa Kouji、Hirakida Takehiro
Coq 中的一些领域理论和指称语义
DOI：
10.1007/978-3-642-03359-9_10
发表时间：
2009
期刊：
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Nick Benton;A. Kennedy;C. Varming
通讯作者：
C. Varming
函数式 BSP 程序的演算
影响因子：
1.3
作者：
F. Loulergue;G. Hains;C. Foisy
通讯作者：
C. Foisy