3 Search Results for "Serpette, Bernard"

Document
DOI: 10.4230/OASIcs.Gabbrielli.10
Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages

Authors: Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.
Cite as

Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito. Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{deboer_et_al:OASIcs.Gabbrielli.10,
  author =	{de Boer, Frank S. and Johnsen, Einar Broch and Schlatte, Rudolf and Tapia Tarifa, Silvia Lizeth and Tveito, Lars},
  title =	{{Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{10:1--10:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.10},
  URN =		{urn:nbn:de:0030-drops-132322},
  doi =		{10.4230/OASIcs.Gabbrielli.10},
  annote =	{Keywords: Testing, Symbolic Traces, Guarded Commands, Partial Order Reduction}
}
Document
DOI: 10.4230/DARTS.3.2.9
Type Abstraction for Relaxed Noninterference (Artifact)

Authors: Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
This artifact is a web interpreter for the ObSec language defined in the companion paper. ObSec is a simple object-oriented language that supports type-based declassification. Type-base declassification exploits the familiar notion of type abstraction to support expressive declassification policies in a simple and expressive manner.
Cite as

Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter. Type Abstraction for Relaxed Noninterference (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{cruz_et_al:DARTS.3.2.9,
  author =	{Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
  title =	{{Type Abstraction for Relaxed Noninterference (Artifact)}},
  pages =	{9:1--9:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.9},
  URN =		{urn:nbn:de:0030-drops-72902},
  doi =		{10.4230/DARTS.3.2.9},
  annote =	{Keywords: type abstraction, relaxed noninterference, information flow control}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.7
Type Abstraction for Relaxed Noninterference

Authors: Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Information-flow security typing statically prevents confidential information to leak to public channels. The fundamental information flow property, known as noninterference, states that a public observer cannot learn anything from private data. As attractive as it is from a theoretical viewpoint, noninterference is impractical: real systems need to intentionally declassify some information, selectively. Among the different information flow approaches to declassification, a particularly expressive approach was proposed by Li and Zdancewic, enforcing a notion of relaxed noninterference by allowing programmers to specify declassification policies that capture the intended manner in which public information can be computed from private data. This paper shows how we can exploit the familiar notion of type abstraction to support expressive declassification policies in a simpler, yet more expressive manner. In particular, the type-based approach to declassification---which we develop in an object-oriented setting---addresses several issues and challenges with respect to prior work, including a simple notion of label ordering based on subtyping, support for recursive declassification policies, and a local, modular reasoning principle for relaxed noninterference. This work paves the way for integrating declassification policies in practical security-typed languages.
Cite as

Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter. Type Abstraction for Relaxed Noninterference. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 7:1-7:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cruz_et_al:LIPIcs.ECOOP.2017.7,
  author =	{Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
  title =	{{Type Abstraction for Relaxed Noninterference}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{7:1--7:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.7},
  URN =		{urn:nbn:de:0030-drops-72688},
  doi =		{10.4230/LIPIcs.ECOOP.2017.7},
  annote =	{Keywords: type abstraction, relaxed noninterference, information flow control}
}
  • Refine by Type
  • 3 Document/PDF

  • Refine by Publication Year
  • 1 2020
  • 2 2017

  • Refine by Author
  • 2 Cruz, Raimil
  • 2 Rezk, Tamara
  • 2 Serpette, Bernard
  • 2 Tanter, Éric
  • 1 Johnsen, Einar Broch
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 OASIcs
  • 1 DARTS

  • Refine by Classification
  • 1 Software and its engineering → Automated static analysis
  • 1 Software and its engineering → Semantics
  • 1 Software and its engineering → Software testing and debugging
  • 1 Theory of computation → Semantics and reasoning

  • Refine by Keyword
  • 2 information flow control
  • 2 relaxed noninterference
  • 2 type abstraction
  • 1 Guarded Commands
  • 1 Partial Order Reduction
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact