Showing 1–3 of 3 results for author: Guernic, G L

Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework

Authors: Gurvan Le Guernic, Benoit Combemale, José A. Galindo

Abstract: Many project-specific languages, including in particular filtering languages, are defined using non-formal specifications written in natural languages. This leads to ambiguities and errors in the specification of those languages. This paper reports on an industrial experiment on using a tool-supported language specification framework (K) for the formal specification of the syntax and semantics of… ▽ More Many project-specific languages, including in particular filtering languages, are defined using non-formal specifications written in natural languages. This leads to ambiguities and errors in the specification of those languages. This paper reports on an industrial experiment on using a tool-supported language specification framework (K) for the formal specification of the syntax and semantics of a filtering language having a complexity similar to those of real-life projects. This experimentation aims at estimating, in a specific industrial setting, the difficulty and benefits of formally specifying a packet filtering language using a tool-supported formal approach. △ Less

Submitted 29 January, 2017; originally announced January 2017.

Comments: In Proceedings F-IDE 2016, arXiv:1701.07925

Journal ref: EPTCS 240, 2017, pp. 38-52

In my Wish List, an Automated Tool for Fail-Secure Design Analysis: an Alloy-Based Feasibility Draft

Authors: Gurvan Le Guernic

Abstract: A system is said to be fail-secure, sometimes confused with fail-safe, if it maintains its security requirements even in the event of some faults. Fail-secure analyses are required by some validation schemes, such as some Common Criteria or NATO certifications. However, it is an aspect of security which as been overlooked by the community. This paper attempts to shed some light on the fail-secure… ▽ More A system is said to be fail-secure, sometimes confused with fail-safe, if it maintains its security requirements even in the event of some faults. Fail-secure analyses are required by some validation schemes, such as some Common Criteria or NATO certifications. However, it is an aspect of security which as been overlooked by the community. This paper attempts to shed some light on the fail-secure field of study by: giving a definition of fail-secure as used in those certification schemes, and emphasizing the differences with fail-safe; and exhibiting a first feasibility draft of a fail-secure design analysis tool based on the Alloy model checker. △ Less

Submitted 5 May, 2014; originally announced May 2014.

Comments: In Proceedings ESSS 2014, arXiv:1405.0554

ACM Class: C.4 [Performance of Systems] --- Design studies, Fault tolerance, Modeling techniques; B.8.1 [Performance and Reliability]: Reliability, Testing, and Fault-Tolerance

Journal ref: EPTCS 150, 2014, pp. 50-55

Epistemic Temporal Logic for Information Flow Security

Authors: Musard Balliu, Mads Dam, Gurvan Le Guernic

Abstract: Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing pro… ▽ More Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways. △ Less

Submitted 30 August, 2012; originally announced August 2012.

Comments: Published in PLAS 2011