A Conference Management System with Verified Document Confidentiality
A Conference Management System with Verified Document Confidentiality
复制标题
具有文件机密性验证的会议管理系统
DOI：
10.1007/978-3-319-08867-9_11
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
A. Popescu
中科院分区：
文献类型：
--
作者：
Sudeep Kanav;P. Lammich;A. Popescu
我们提出了对现实系统的验证安全性的案例研究：会议管理系统的实施，其功能性内核忠实地在Isabelle Theorem Prover中表示，我们在其中指定并验证机密性属性。这种开发带来的各种理论和实用挑战导致了一种新型的安全模型和验证方法，通常适用于可描述为InputOutput自动机的系统。
We present a case study in verified security for realistic systems: the implementation of a conference management system, whose functional kernel is faithfully represented in the Isabelle theorem prover, where we specify and verify confidentiality properties. The various theoretical and practical challenges posed by this development led to a novel security model and verification method generally applicable to systems describable as inputoutput automata.
DOI：
10.1007/978-3-642-27940-9_12
发表时间：
2012-01
期刊：
--
影响因子：
--
作者：
Rayna Dimitrova;B. Finkbeiner;Máté Kovács;M. Rabe;H. Seidl
通讯作者：
Rayna Dimitrova;B. Finkbeiner;Máté Kovács;M. Rabe;H. Seidl