2 Search Results for "Klein, Gerwin"


Document
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security

Authors: Robert Sison and Toby Murray

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations. In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program.

Cite as

Robert Sison and Toby Murray. Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{sison_et_al:LIPIcs.ITP.2019.27,
  author =	{Sison, Robert and Murray, Toby},
  title =	{{Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{27:1--27:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.27},
  URN =		{urn:nbn:de:0030-drops-110829},
  doi =		{10.4230/LIPIcs.ITP.2019.27},
  annote =	{Keywords: Secure compilation, Information flow security, Concurrency, Verification}
}
Document
Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)

Authors: Darren Cofer, Gerwin Klein, Konrad Slind, and Virginie Wiels

Published in: Dagstuhl Reports, Volume 5, Issue 4 (2015)


Abstract
Formal methods tools have been shown to be effective at finding defects in and verifying the correctness of safety-critical systems, many of which require some form of certification. However, there are still many issues that must be addressed before formal verification tools can be used as part of the certification of safety-critical systems. For example, most developers of avionics systems are unfamiliar with which formal methods tools are most appropriate for different problem domains. Different levels of expertise are necessary to use these tools effectively and correctly. In most certification processes, a tool used to meet process objectives must be qualified. The qualification of formal verification tools will likely pose unique challenges.

Cite as

Darren Cofer, Gerwin Klein, Konrad Slind, and Virginie Wiels. Qualification of Formal Methods Tools (Dagstuhl Seminar 15182). In Dagstuhl Reports, Volume 5, Issue 4, pp. 142-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{cofer_et_al:DagRep.5.4.142,
  author =	{Cofer, Darren and Klein, Gerwin and Slind, Konrad and Wiels, Virginie},
  title =	{{Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)}},
  pages =	{142--159},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{4},
  editor =	{Cofer, Darren and Klein, Gerwin and Slind, Konrad and Wiels, Virginie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.4.142},
  URN =		{urn:nbn:de:0030-drops-53543},
  doi =		{10.4230/DagRep.5.4.142},
  annote =	{Keywords: Dependable systems, Certification, Qualification, Formal methods, Verification tools}
}
  • Refine by Author
  • 1 Cofer, Darren
  • 1 Klein, Gerwin
  • 1 Murray, Toby
  • 1 Sison, Robert
  • 1 Slind, Konrad
  • Show More...

  • Refine by Classification
  • 1 Security and privacy → Information flow control
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Compilers

  • Refine by Keyword
  • 1 Certification
  • 1 Concurrency
  • 1 Dependable systems
  • 1 Formal methods
  • 1 Information flow security
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2015
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail