Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP 2021-1


view this post on Zulip Email Gateway (Dec 14 2021 at 10:25):

From: Gerwin Klein <kleing@unsw.edu.au>
The AFP is now available for Isabelle2021-1 from https://isa-afp.org

There are now more than 3.2 million lines of Isabelle proof in 644 entries by 414 authors.

The following set of related entries that were previously in the development version are now available from the front page.

Enjoy!
Gerwin

Compositional BD Security
=========================
by Thomas Bauereiss and Andrei Popescu

This entry contains the confidentiality verification of the (functional kernel
of) the CoCon conference management system [1, 2]. The confidentiality
properties refer to the documents managed by the system, namely papers,
reviews, discussion logs and acceptance/rejection decisions, and also to the
assignment of reviewers to papers. They have all been formulated as instances
of BD Security [3, 4] and verified using the BD Security unwinding technique.

[1]: https://doi.org/10.1007/978-3-319-08867-9_11
[2]: https://doi.org/10.1007/978-3-319-08867-9_11
[3]: https://doi.org/10.4230/LIPIcs.ITP.2021.3
[4]: https://www.isa-afp.org/entries/Bounded_Deducibility_Security.html

https://www.isa-afp.org/entries/BD_Security_Compositional.html

CoCon: A Confidentiality-Verified Conference Management System
==============================================================
by Andrei Popescu, Peter Lammich, and Thomas Bauereiss

Building on a previous AFP entry [0] that formalizes the Bounded-Deducibility
Security (BD Security) framework [1], we formalize compositionality and
transport theorems for information flow security. These results allow lifting
BD Security properties from individual components specified as transition
systems, to a composition of systems specified as communicating products of
transition systems. The underlying ideas of these results are presented in the
papers [1] and [2]. The latter paper also describes a major case study where
these results have been used: on verifying the CoSMeDis distributed social
media platform (itself formalized as an AFP entry [3] that builds on this
entry).

[0]: https://www.isa-afp.org/entries/Bounded_Deducibility_Security.html
[1]: https://doi.org/10.4230/LIPIcs.ITP.2021.3
[2]: https://doi.org/10.1109/SP.2017.24
[3]: https://www.isa-afp.org/entries/CoSMeDis.html

https://www.isa-afp.org/entries/CoCon.html

CoSMed: A confidentiality-verified social media platform
========================================================
by Thomas Bauereiss and Andrei Popescu

This entry contains the confidentiality verification of the (functional kernel
of) the CoSMed social media platform. The confidentiality properties are
formalized as instances of BD Security [1, 2]. An innovation in the deployment
of BD Security compared to previous work is the use of dynamic
declassification triggers, incorporated as part of inductive bounds, for
providing stronger guarantees that account for the repeated opening and
closing of access windows. To further strengthen the confidentiality
guarantees, we also prove "traceback" properties about the accessibility
decisions affecting the information managed by the system.

[1]: https://doi.org/10.4230/LIPIcs.ITP.2021.3
[2]: https://www.isa-afp.org/entries/Bounded_Deducibility_Security.html

https://www.isa-afp.org/entries/CoSMed.html

CoSMeDis: A confidentiality-verified distributed social media platform
======================================================================
by Thomas Bauereiss and Andrei Popescu

This entry contains the confidentiality verification of the (functional kernel
of) the CoSMeDis distributed social media platform presented in [1]. CoSMeDis
is a multi-node extension the CoSMed prototype social media platform [2, 3,
4]. The confidentiality properties are formalized as instances of BD Security
[5, 6]. The lifting of confidentiality properties from single nodes to the
entire CoSMeDis network is performed using compositionality and transport
theorems for BD Security, which are described in [1] and formalized in a
separate AFP entry [7].

[1]: https://doi.org/10.1109/SP.2017.24
[2]: https://doi.org/10.1007/978-3-319-43144-4_6
[3]: https://doi.org/10.1007/s10817-017-9443-3
[4]: https://www.isa-afp.org/entries/CoSMed.html
[5]: https://doi.org/10.4230/LIPIcs.ITP.2021.3
[6]: https://www.isa-afp.org/entries/Bounded_Deducibility_Security.html
[7]: https://www.isa-afp.org/entries/BD_Security_Compositional.html

https://www.isa-afp.org/entries/CoSMedDis.html


Last updated: Mar 29 2024 at 08:18 UTC