CoCon: A Conference Management System with Formally Verified Document Confidentiality
| Autor: | Andrei Popescu, Ping Hou, Peter Lammich |
|---|---|
| Přispěvatelé: | Digital Society Institute, Formal Methods and Tools |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Computer science
business.industry 020206 networking & telecommunications 020207 software engineering 02 engineering and technology Computer security model Automaton Automated theorem proving Development (topology) Computational Theory and Mathematics Kernel (image processing) Artificial Intelligence 0202 electrical engineering electronic engineering information engineering Web application Confidentiality Information flow (information theory) business Software engineering Software |
| Zdroj: | Popescu, A, Lammich, P & Hou, P 2020, ' CoCon: A Conference Management System with Formally Verified Document Confidentiality ', Journal of Automated Reasoning . https://doi.org/10.1007/s10817-020-09566-9 Journal of automated reasoning, 65(2), 321-356. Springer |
| ISSN: | 0168-7433 |
| Popis: | We present a case study in formally verified security for realistic systems: the information flow security verification of the functional kernel of a web application, the CoCon conference management system. We use the Isabelle theorem prover to specify and verify fine-grained confidentiality properties, as well as complementary safety and “traceback” properties. The challenges posed by this development in terms of expressiveness have led to bounded-deducibility security, a novel security model and verification method generally applicable to systems describable as input/output automata. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink