Yliès Falcone

Laurent Mounier

Jean-Claude Fernandez

Jean-Luc Richier

j-POST: a Java Toolchain for Property-Oriented Software Testing

Keywords: property testing, tool, composition, Java

j-POST is an integrated toolchain for property-oriented software testing. This toolchain includes a test designer, a test generator, and a test execution engine. The test generation is based on an original approach which consists of deriving a set of communicating test processes obtained both from a requirement formula (expressed in a trace-based logic) and a behavioral specification of some specific parts of the software under test. The test execution engine is then able to coordinate the execution of these test processes against a distributed Java program. j-POST was applied to check the correct deployment of a security policy for a travel management application.

Introduction

Testing is a validation technique aimed to find defective behaviours on a system either during its development, or once a final version is issued. It remains one of the most feasible methodologies to ensure the expected behaviour of a software. This is notably due to its ability to cope with continual growth of system complexity. However, reducing its cost and time consumption remains a very important challenge sustained by a strong industrial demand.

In previous work [START_REF] Falcone | A Test Calculus Framework Applied to Network Security Policies[END_REF][START_REF] Falcone | A Compositional Testing Framework Driven by Partial Specifications[END_REF] we have presented a black-box test generation method able to construct abstract test cases from a formal requirement (a property that the system is expected to fulfill). This method (implemented in a prototype tool) is based on a test calculus allowing the method to be compositionally and formally defined. In this framework, a requirement is expressed by a logical formula built upon a set of (abstract) predicates. Each predicate corresponds to a (possibly nonatomic) operation to be performed on the system under test, and is user-provided as a test module indicating how to perform this operation on the actual implementation, and how to decide whether its execution succeeds or not. The test generation step consists in building, by composition of test modules, a set of communicating test processes from this property. In this paper we present a significant step from this previous work. First off, we present formally how the previously generated test can be executed. Besides we present j-POST, an integrated toolchain for propertyoriented software testing. In addition to a full implementation of the test generation tool, we present the associated test designer and test execution engine resulting in a fully integrated toolchain. The test designer helps the user to provide inputs to the test generator. The test execution engine is able to coordinate the execution of the generated processes against a possibly distributed program, leading to a satisfiability verdict with respect to the given requirement.

Comparison with classical model-based testing.

This approach offers several advantages over more classical model-based test generation techniques [START_REF] Tretmans | Test Generation with Inputs, Outputs and Repetitive Quiescence[END_REF] implemented in several existing tools (e.g. TGV [START_REF] Jard | TGV: theory, principles and algorithms, A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems[END_REF], TorX [START_REF] Tretmans | TorX: Automated Model Based Testing -Côte de Resyste[END_REF], see [START_REF] Belinfante | Tools for Test Case Generation[END_REF][START_REF] Hartman | Model Based Test Generation Tools Survey[END_REF] for more exhaustive surveys). First, j-POST is able to deal with piecewise specifications restricted to specific functionalities. We strongly believe that this feature is really important in practice, especially in application domains where formal modeling of software is not a common practice. Specifying only some global requirement and some specific implementation features in an operational way (i.e. the test modules) seems much easier for test engineers than building a complete model of a software. As a consequence, the test generation step will not require the exploration of such a complete model, avoiding the well-known state explosion problem. Furthermore, this toolchain remains open in the sense that various logics can be considered to express the requirements, and new logic plugins can be easily added. Finally, this toolchain integrates a large spectrum of the whole test process, from the test design to the test execution.

The remainder of this paper is organized as follows. Sect. 2 describes the underlying theory of j-POST and Sect. 3 describes the toolchain itself. In Sect. 4, we depict one of the experiments conducted with j-POST on a travel agency application. Sect. 5 exposes some conclusions and perspectives opened by this work.

Underlying testing theory

This section briefly presents the background of j-POST, namely how to produce and execute test cases from a formal requirement following a syntax-driven approach. More details can be found in the research reports available in [8].

We consider in the following that the behaviour of the software under test (SUT) can be modelled using a labelled transition system (LTS), noted Sut, namely a quadruplet (Q Sut , Act Sut , →, q 0 ) where Q is a set of states, Act Sut a set of actions (labels), →⊆ Q Sut × Act Sut × Q Sut the transition relation and q 0 ∈ Q Sut the initial state. In black-box testing this behaviour can be accessed only through a SUT interface, namely a set of visible actions Act vis ⊆ Act Sut . Non visible actions are supposed to be labelled by τ . We will denote by p a -→ q when (p, a, q) ∈→, and by p 1 τ * a =⇒ q when there exist p 2 , p 3 , . . . , p n s.t. p i τ -→ p i+1 and p n a -→ q. Finally, we define the execution sequences of Sut as the set of finite sequences of visible actions that can be performed from its initial state:

Exec(Sut) = {a 1 .a 2 . • • • .a n | ∃q 1 , . . . , q n+1 s.t. q i τ * a i =⇒ q i+1 ∧ q 1 = q 0 }.

The properties to test

We assume in the following that the properties to test are expressed using a logic L . Formulas of L are built upon a finite set of n-ary operators F n and a finite set of predicates {p 1 , p 2 , . . . , p n }. The abstract syntax of such a logic could be defined as follows: formula ::= F n (formula 1 , formula 2 , . . . , formula n ) | p i .

Formulas of L are interpreted over finite execution sequences. However, this semantics also takes into account two other important features:

• First, this semantics is defined on two levels. Predicates are not atomic, i.e. they do not necessarily correspond to occurrences of single visible actions, but rather of (concrete) sequences of visible actions. Operators F n are then interpreted over abstract execution sequences, i.e., sequences of predicates.

• Second, since our objective is to test either the validity or the non-validity of a formula ϕ, the semantics of ϕ defines three kinds of execution sequences, corresponding to the possible verdicts delivered by a tester: the ones that satisfy ϕ (pass), the ones that do not satisfy ϕ (fail), and the ones for which we cannot conclude about the satisfiability of ϕ (inconc).

More formally, a triplet of finite languages (L P p i , L F p i , L I p i ) is associated with each predicate p i . These three languages define respectively concrete execution sequences that satisfy p i , that do not satisfy p i , and for which the satisfiability of p i is unknown. The following assumptions are required:

• L P p i , L F p i and L I p i are defined over an alphabet A p i ⊆ Act vis . Intuitively, A p i is the set of visible actions whose occurrences influence the truth value of p i .

• This set of three languages defines a partition of (A p i ) * .

• For two distinct predicates p i , p j , A p i and A p j are disjoint.

The semantics of a non-atomic formula ϕ(p 1 , p 2 , . . . , p n ) is then defined by three sets

[[ϕ]] P , [[ϕ]] F , [[ϕ]] I , inductively computed from L P p i , L F p i and L I p i for each p i appearing in ϕ.
Finally, we say that an LTS S satisfies ϕ (we note S |= ϕ) iff all sequences of Exec(S) belong to [[ϕ]] P , and we say that it does not satisfy ϕ iff there exists a sequence of Exec(S) that belongs to [[ϕ]] F .

A set of communicating test processes

The test cases we aim to produce consist of a set of sequential communicating test processes. Roughly speaking, each test process is built from classical programming primitives such as variable assignment, sequential composition, (non-deterministic) choice, and iteration. It can also perform communications with the other test processes, and interact with the SUT. This sequential behaviour can be modelled by an LTS extended with variables.

Test processes run asynchronously and communicate with each other either by "rendez-vous" on dedicated communication channels or through shared variables. The semantics of a whole test process T ϕ can be expressed by an LTS S Tϕ . A complete syntax and semantics of such a "test calculus" can be found in [START_REF] Falcone | A Test Calculus Framework Applied to Network Security Policies[END_REF], but other classical process algebra could be used as well.

Test generation

The purpose of the test generation phase [START_REF] Falcone | A Compositional Testing Framework Driven by Partial Specifications[END_REF] is to produce a test case T ϕ (i.e. a set of communicating test processes) associated to the L -formula ϕ under test. We distinguish two kinds of test processes (which are both LTSs):

• test modules t p i , provided by the user, and associated with the predicates p i of ϕ. Their purpose is to produce a test verdict indicating whether a given concrete execution sequence belongs either to

L P p i , L F p i or L I p i .
Examples of such test modules are given on Fig. 5 in Sect. 4.

• test controllers t F n , associated with each n-ary operator F n of the logic L . Their purpose is to control the execution of the test process associated to each of their operands by means of basic signals (start, stop, loop), and to collect their verdicts in order to produce a resulting verdict corresponding to this instance of operator F n . One can find controllers for several logics in the research reports provided in [8].

This test generation technique can be formalized by a function called GenTest L , such that GenTest L (ϕ) = T ϕ . This function is inductively defined on the syntax of L in the following way:

• If ϕ = p i , then GenTest L (ϕ) returns the test module t p i (associated with the predicate p i ) extended with the communication operations required to make it controlable by another test process (see Fig. 3 in Sect. 3).

• If ϕ = F n (ϕ 1 , • • • , ϕ n ), then GenTest L (ϕ)
returns a parallel composition between (recursively defined) test processes t ϕ 1 , . . . , t ϕn and an instance of the (generic) test controller t F n .

Finally, a special test process t main is added to launch the whole test execution and collect the final verdict. According to this generation technique, the architecture of a test case T ϕ exactly matches the abstract syntax tree corresponding to formula ϕ: the root is t main , leaves are test modules corresponding to predicates p i of ϕ, and intermediate nodes are controllers associated with operators of ϕ (see Fig. 6 in Sect. 4.2 for an example).

Test selection and execution

From a formal point of view, the test execution sequences are the execution sequences of a parallel composition between the LTS S modelling the SUT behaviour and the test case S Tϕ , with a "rendez-vous" synchronization on the visible actions appearing in S Tϕ .

However, this LTS product may still contain a bunch of possible test executions (due to possible non-determinism both inside the test modules and introduced by the parallel composition). Moreover, the test generation function only ensures that the verdicts produced by the test execution are sound with respect to the initial formula ϕ: it does not help to select the interesting test executions that are likely to exhibit an incorrect behaviour of the SUT. To solve this problem we propose to use behavioural test objectives, already introduced in several model-based testing tools (e.g. in [START_REF] Jard | TGV: theory, principles and algorithms, A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems[END_REF][START_REF] Schmitt | Test Generation with Autolink and Testcomposer[END_REF]). Their purpose is to inject some execution scenario in the test cases produced by the test generation phase, either by enforcing the execution order of some visible actions, or by introducing other additional visible actions to lead the SUT into some particular state. Most of the time, in specification based testing, this test selection is performed during the test generation phase, by pruning the undesired test executions from the whole SUT specification. In our approach, the selection is not performed during test generation, but during the test execution (similarly to walk guidance in TorX). This is due to the fact that we do not rely on such a specification. So, the test selection phase is combined with the test execution: the test objective is expressed by an LTS with accepting states, and the test sequences leading to such states are privileged during the text execution.

This approach is formalized below. In a LTS S, for two states q, q ′ we note q ′ ∈ Reach S (q) the fact that q ′ is accessible from q in S. Also, when q ′ ∈ Reach S (q), we note d S (q, q ′ ) the distance between q and q ′ , i.e. the minimal length of the existing paths between q and q ′ . Definition 2.1 [Behavioural test objective] A test objective O relatively to a test case t which semantics can be expressed by a LTS (Q

St , Act St , → St , q St 0 ) is a de- terministic LTS (Q O , Act O , → O , q O 0 ) complete wrt. Act St (i.e. ∀q ∈ Q St , ∀a ∈ Act St , ∃q ′ ∈ Q O • q a → O q ′ ). Q O contains
= (Q O , Act O , → O , q O 0 )
. The execution of t guided by O can be defined as a synchronous product

S O t = S t × O such as Act S O t = Act O , Q S O t ⊆ Q St × Q O ∪ Inc, and → S O
t is defined by the following rules. Note that control and observation actions are not distinguished.

t a → S t t ′ Accept O ∈ Reach O (o), o a → O o ′ d S (o ′ , Accept O ) < d S (o, Accept O ), a ∈ Act S t (1) (t, o) a → S O t (t ′ , o ′ )
Accept O ∈ Reach O (o), o a → S O o ′ d S (o ′ , Accept O ) < d S (o, Accept O ), a / ∈ Act S t (1 ′ ) (t, o) a → S O t (t, o ′ ) t a → S t t ′ Accept O ∈ Reach O (o), o a → O o ′ d S (o ′ , Accept O ) ≥ d S (o, Accept O ) (2) (t, o) a → S O t (t ′ , o ′ ) o a → O Reject O (3) (t, o) a → S O t Inc
Some priorities are associated with these rules to favour the execution of transitions bringing closer to an Accept state. The rules (1) and ( 2) are of the highest prioriy, then is rule (2), and at last the rule (3) is of the lowest priority.

Finally, the set of test execution sequences obtained from an SUT S and a test case S Tϕ when taking into account a test objective O is defined as the execution sequences of the parallel composition between the SUT S and the LTS S Tϕ × O. Note that when the Inc state is reached in this composition, the whole test execution is stopped and an inconclusive verdict is issued. This general framework has been instantiated for two particular logics, namely LTL-X, and extended regular expressions (see Sect. 3.2).

Architecture and functionalities of j-POST

The architecture of the toolchain is depicted in Fig. 1. It is built upon three main components, a test designer, a test generator and a test execution engine. Two interfaces are provided: a command-line mode and a graphic interface.

The purpose of j-POST is to check through black-box testing whether a Java application fulfills a given requirement. To do so, the test designer (step 1) helps the user both to formalize this requirement in a trace-based logic and to elaborate a test module library. Each test module (corresponding to a predicate used in the requirement) is obtained by combining some of the actions offered by the SUT interface. The test modules are used by the test generator (step 2), according to a logic plugin, to produce a test case as a set of communicating test processes. Finally, this test case can be launched by the test engine (step 3), taking into account a test objective to select the more promising test sequences.

Test designer

The test designer of j-POST is a user assistant that helps to elaborate the formal requirements and the corresponding test modules through dedicated editors available within the Eclipse Modeling Framework. Each test module is stored into an XML file (their j-POST internal representation). Moreover, the test designer provides

F (p i ) ∈ ERE, LT L p i ↔ m i m 1 • • • m n communicating
Fig. 2. Abstract view of the j-POST test designer and test generator architecture a tool (based on GraphViz [START_REF]Graph Visualization Software[END_REF]) to vizualise them in a more intelligible way. This avoids any error-prone manipulations of XML files from the user.

Test generator

The j-POST test generator consists mainly in implementing the GenT est L function.

It produces a test case following the syntax-driven approach recalled in Sect. 2.3 in two stages:

The first stage is the construction of a communication tree obtained from the abstract syntax tree of the formula. This tree expresses the communication architecture between the test processes that will be produced by the test generator. Its leaves are abstract test modules (ATM) corresponding to the atomic predicates of the formula, taken from the library. Its internal nodes are (copies of) generic test controllers, corresponding to the logical operators appearing in the formula (they are obtained from a finite set of generic controllers provided by the logic plugin). Finally, the root of this tree is a special test process, called testCaseLauncher, whose purpose is to initiate the test execution and deliver the resulting verdict.

The second stage consists of instantiating the communication tree by associating fresh channel names to each local communication between test processes. It relies on a traversal of this communication tree in order to modify the test modules. In particular the test modules provided by the user are automatically extended with additional communication actions to be managed by the test controllers, e.g. starting signal, verdict emission (see Fig. 3). The resulting test case is a set of XML files, one per test process.

Generic test controllers and test generation algorithms have been defined for different specification formalisms. So far, j-POST TestGenerator supports two common-use formalisms, by means of logic plugins:

• Temporal logics [START_REF] Manna | Temporal verification of reactive systems: safety[END_REF] like LTL are frequently used in the verification community to express requirements on reactive systems. We consider here fragments of such logics whose models are set of finite execution traces. We did not include the next operator in order to be insensitive to stuttering [START_REF] Clarke | Model Checking[END_REF]. The complete definition of the variant of LTL-X we use is given in [START_REF] Falcone | A Compositional Testing Framework Driven by Partial Specifications[END_REF].

• Extended Regular Expressions [START_REF] Kleene | Representation of events in nerve nets and finite automata[END_REF] are another formalism to define behavior pat-

Test execution engine

The purpose of the test execution engine is to produce a verdict for the initial requirement. It takes as inputs the test case produced by the test generator, a test objective, and a mapping describing how to execute SUT interactions used in the test modules. The architecture of the engine is depicted in Fig. 4. First the test case (a set of XML files) is loaded using the test case loader. Each test process is executed in a separate Java thread. A centralized scheduler implements both the internal communications between the test processes (based on "rendez-vous" and shared variables), and solves the priority conflicts between their actions (according to a predefined policy). Moreover, interactions to be performed on the SUT transit through a Concretisation Wrapper. This component is in charge of transforming these interactions into executable operations on the SUT (depending on the communication medium used, e.g. Java RMI). This transformation may also add some parameters omitted at the test module level (for the sake of simplicity), but mandatory for the test execution. Finally, the test selection operation described in Sect. 2.4 is performed by the Objective Engine. When the test execution terminates a verdict is issued and the Logger produces some execution traces that help the diagnostic phase.

j-POST at work

We describe in this section the use of j-POST on an example. Tests are designed, generated, executed using the j-POST toolchain to check some properties on a travel agency application [START_REF] Falcone | A Travel Agency Application[END_REF], called Travel. We take as inputs an informal requirement extracted from the functional specification of Travel and the application interface. The requirement we choose for the demonstration purpose is informally expressed as "it is impossible to create a mission in Travel before being connected".

Test design

We start by presenting the test design stage, that is the requirement formalization and the edition of test modules.

Requirement formalization.

A possible understanding of our requirement could be that a behaviour in which it is possible to create a mission before performing the identification action is not desired. In other words, we can say that we require no mission creation until a connection is open. This informal statement refers to two abstract operations: "create a mission", and "open a connection". In the following we respectively designate these two operations by the predicates missionCreation() and connection(). The requirement can be expressed formally by an LTL formula: ( ¬missionCreation( ) ) U connection().

Test module edition.

Test modules have to be created by the user for the predicates missionCreation() and connection(). Each of this module should describe:

• how to perform the abstract operation using the Travel interface;

• what is the test verdict obtained (depending on how Travel reacts).

Possible test modules are proposed in Fig. 5, produced with the j-POST test designer. The connection test module (left-hand side) contains three possible execution sequences: a correct call to the connection method identify (the user is "Falcone", the correct password is "azerty", which corresponds to a registered user of Travel ), an incorrect one (the password is "qwerty", it is not valid), and an execution where the connection procedure is never called. Note that the call to the method returns an identification number which is stored in a shared variable (between test components) called id. The createM ission test module (right-hand side) consists of calling the missionRequest() method, supplying the shared variable id as an identification number. Depending on the return value (createOk), it delivers the corresponding verdict.

Inside the toolchain these modules are represented using an XML format, but, from a practical point of view, they can be written and viewed using the j-POST test designer.

Test generation

The requirement stated, and the test modules designed (Fig. 5), we are now able to perform the test generation. In order to illustrate such a process, we give an insight of the generated test case on Fig. 6. The structure of this test case follows the structure of the formula. It contains a test controller for each operator appearing in the formula (Until and Not), and a test module for each predicate (missionCreation() and Connection()). The testCaseLauncher is in charge of managing the execution of the testcase and emitting the final verdict. The c start (resp. c stop, c loop, c ver) channels are used by the processes to perform starting (resp. stopping, rebooting, verdict transmission) operations.

Test execution

The next operation to perform is to choose a test objective in order to restrict the set of potential test executions. Regarding the requirement we consider ("no mission creation until a connection is open"), an interesting objective is to try to falsify this requirement in order to exhibit an incorrect behaviour of the software under test. Falsifying such a requirement means for instance producing an execution sequence where :

• the verdict delivered by missionCreation() is pass (possibly after several previous fail results) ;

• in the meantime, the verdict delivered by connection() remains always fail.

Such a test objective can be obtained from the test modules given on Fig. 5. However, obtaining a fail verdict for a connection operation can be fully controlled by the test execution engine (e.g., by supplying an incorrect password), whereas the verdict returned by a mission creation cannot be controlled (it only depends on the SUT behaviour).

Three versions of the Travel application have been tested:

• Experiment 1. In the first (erroneous) version of Travel a mission creation request is always accepted, therefore our requirement is false (a mission can be created by a non connected user). The test execution engine detects this error (it delivers a fail verdict) and produces the test execution traces and graphs for the test case and each module.

• Experiment 2. In the second (erroneous) version of Travel a mission creation request is accepted either if the identification number supplied is correct (it corresponds to a return value of a connection request), or if it is the third attempt to create this mission. Therefore our requirement is still false: if a non connected user tries repeatedly to create a mission, it eventually succeeds. This error is detected by the test engine, which delivers a fail verdict.

• Experiment 3. Finally, the third version of Travel always refuses a mission request as long as the identification number supplied is invalid. Thus, the only way for a non connected user to create a mission is to "guess" a correct identification number. This cannot be achieved by our test execution engine, which delivers here a pass verdict.

Conclusion and perspectives

This paper presents an original approach for property-oriented software testing (POST). Starting from a formula expressed in a trace-based logic, the user first provides a test module (using the test designer) dedicated to each predicate appearing in this formula. The test generation phase then consists of producing a test case as a set of communicating test processes by combining the test modules with some test controllers associated to each logical operator. This test case can be executed by a test engine, able to take into account a test objective to constrain the set of test sequences to execute. This whole testing approach has been implemented in a working tool and applied to some non-trivial case studies. The architecture makes it open, and easily allows the toolchain to support new logical formalisms by adding logic plugins.

The main advantage of this approach is that it does not require a "global" behavioural specification of the software under test, as is the case in many modelbased testing approaches. In fact the user only needs to make explicit the evaluation of a predicate in the test modules. The test generation phase is therefore rather straightforward and does not suffer from state explosion limitations. Of course, the test case produced may encompass many possible test executions, but the use of test objective allows the user to select the most interesting scenarios. This approach seems particularly relevant to dealing with security or robustness testing, where the functional model of the SUT can be very large (and hence not easily available as a single formal specification), and where the requirements to be checked only concern specific parts of this model. In fact, one of the motivations for this work was the validation of the correct deployment of security policies within the French Politess [START_REF]Project Politess[END_REF] project.

The Travel case study allowed many enhancements for j-POST and opens several research perspectives. In particular, it appears that the design of test modules could be facilitated by the use of abstract domains (e.g., at the test module level one only needs to distinguish between correct passwords and incorrect ones, without referring to a concrete value). These abstract domains could then be concretized only at the test execution level by selecting relevant values within a concrete domain (which may depend on the SUT's current state). This concretisation could be performed, for instance, according to coverage criteria that could be defined with respect to the requirement under test. It seems particularly worthwile to relate this work with [START_REF] Lestiennes | Testing processes from formal specifications with inputs, outputs and data types[END_REF].

Fig. 1 .

 1 Fig. 1. Abstract view of the j-POST testing toolchain

Fig. 3 .Fig. 4 .

 34 Fig. 3. Instantiation of an abstract test component tp

Fig. 5 .Fig. 6 .

 56 Fig. 5. Test modules for predicates connection and createM ission

  two sink states Accept O and Reject O , and Act O ⊆ Act vis . Using a test objective, it is possible to operate "on the fly" a test selection on the test case during the execution. Definition 2.2 [Selection using a behavioural test objective] Let t be a test case which semantics can be expressed by S t = (Q St , Act St , → St , q St 0 ), and a behavioural test objective O

  F (p i ) ∈ ERE, LT L

			Test Objective	SUT
	Informal	Formal Requirement
	Requirement				Verdict for F
	Test Designer	Generator Test	test cases abstract	Engine Execution Test	(pass,fail,inc)
	SUT Interface	ATM Library p i ↔ t i			Logging information


Yliès Falcone

Jean-Claude Fernandez

Laurent Mounier

Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties

Runtime enforcement is a powerful technique to ensure that a program will respect a given security policy. We extend previous works on this topic in several directions. Firstly, we propose a generic notion of enforcement monitors based on a memory device and finite sets of control states and enforcement operations. Moreover, we specify their enforcement abilities w.r.t. the general safety-progress classification of properties. It allows a fine-grain characterization of the space of enforceable properties. Finally, we propose a systematic technique to produce an enforcement monitor from the Streett automaton recognizing a given safety, guarantee, obligation or response security property.

Introduction

The growing complexity of nowadays programs and systems induces a rise of needs in validation. With the enhancement of engineering methods, software components tend to be more and more reusable. Although this trend clearly improves programmers productivity, it also raises some important security issues. Indeed, each individual component should guarantee some individual properties at run-time to ensure that the whole application will respect some given security policy. When retrieving an external component, the question of how this code meets a set of proper requirements raises. Using formal methods appears as a solution to provide techniques to regain the needed confidence. However, these techniques should remain practical enough to be adopted by software engineers.

Runtime monitoring falls it this category. It consists in supervising at runtime the execution of an underlying program against a set of expected properties. With an appointed monitor, one is able to detect any occurrence of specific property violations. Such a detection might be a sufficient assurance. However, for certain kind of systems a misbehavior might be not acceptable. To prevent this, a possible solution is then to enforce the desired property: the monitor not only observe the current program execution, but it also controls it in order to ensure that the expected property is fulfilled. Such a control should usually remain transparent, meaning that it should leave any original execution sequence unchanged when already correct, or output its longest correct prefix otherwise.

Runtime enforcement monitoring was initiated by the work of Schneider [START_REF] Schneider | Enforceable security policies[END_REF] on what has been called security automata. In this work the monitors watch the current execution sequence and halt the underlying program whenever it deviates from the desired property. Such security automata are able to enforce the class of safety properties [START_REF] Hamlen | Computability classes for enforcement mechanisms[END_REF], stating that something bad can never happen. Later, Viswanathan [START_REF] Viswanathan | Foundations for the run-time analysis of software systems[END_REF] noticed that the class of enforceable properties is impacted by the computational power of the enforcement monitor: since the enforcement mechanism cannot implement more than computable functions, only decidable properties can be enforced. More recently [START_REF] Ligatti | Runtime Enforcement of Nonsafety Policies[END_REF][START_REF] Ligatti | Enforcing non-safety security policies with program monitors[END_REF], Ligatti and al. showed that it is possible to enforce at runtime more than safety properties. Using a more powerful enforcement mechanism called edit-automata, it is possible to enforce the larger class of infinite renewal properties, able to express some kinds of obligations used in security policies. More than simply halting an underlying program, editautomata can also "suppress" (i.e., froze) and "insert" (frozen) actions in the current execution sequence. To better cope with practical resource constraints, Fong [START_REF] Fong | Access control by tracking shallow execution history[END_REF] studied the effect of memory limitations on enforcement mechanisms. He introduced the notion of Shallow History Automata which are only aware of the occurrence of past events, and do not keep any information about the order of their arrival. He showed that such a "shallow history" indeed leads to some computational limitations for the enforced properties. However, many interesting properties remain enforceable using shallow history automata.

In this paper, we propose to extend these previous works in several directions. Firstly, we study the enforcement capabilities relatively to the so-called safetyprogress hierarchy of properties [START_REF] Chang | The safety-progress classification[END_REF][START_REF] Chang | Characterization of temporal property classes[END_REF]. This classification differs from the more classical safety-liveness classification [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF][START_REF] Alpern | Defining liveness[END_REF] by offering a rather clear characterization of a number of interesting kinds of properties (e.g. obligation, accessibility, justice, etc.), particularly relevant in the security context. Moreover this classification features properties, such as transactional properties (i.e, an action pattern to be repeated infinitely), which are neither safety nor liveness properties. Thus, using this classification as a basis provides a finer-grain classification of enforceable properties. Moreover, in this safety-progress hierarchy, each property ϕ can be characterized by a particular kind of (finite state) recognizing automaton A ϕ . Secondly, we show how to generate an enforcement monitor for ϕ in a systematic way, from a recognizing automaton A ϕ . This enforcement monitor is based on a finite set of control states, and an auxiliary memory. This general notion of enforcement monitor encompasses the previous notions of security automata, edit-automata and "shallow history" automata. The companion report [START_REF] Falcone | Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties[END_REF] exposes more details and complete proofs of the theorems of this paper.

The remainder of this article is organized as follows. The Sect. 2 introduces some preliminary notions for our work. In Sect. 3 we recall briefly the necessary elements from the safety-progress classification of properties. Then, we present our notion of enforcement monitor and their properties in Sect. 4. The Sect. 5 studies the enforcement capability wrt. the safety-progress classification. Sect. 6 discusses some implementation issues. Finally, the Sect. 7 exposes some concluding remarks. This section introduces some preliminary notations, namely the notions of program execution sequences and program properties we will consider in the remainder of this article.

Sequences, and execution sequences

Sequences. Considering a finite set of elements E, we define notations about sequences of elements belonging to E. A sequence σ containing elements of E is formally defined by a function σ : N → E where N is the set of natural numbers. We denote by E * the set of finite sequences over E (partial function from N), and by E ω the set of infinite sequences over E (total function from N). The set E ∞ = E * ∪ E ω is the set of all sequences (finite or not) over E. The empty sequence is denoted ǫ. The length (number of elements) of a finite sequence σ is noted |σ| and the (i + 1)-th element of σ is denoted by σ i . For two sequences σ ∈ E * , σ ′ ∈ E ∞ , we denote by σ • σ ′ the concatenation of σ and σ ′ , and by σ ≺ σ ′ (resp. σ ′ ≻ σ) the fact that σ is a strict prefix of σ ′ (resp. σ ′ is a strict suffix of σ). The sequence σ is said to be a strict prefix of σ ′ when ∀i ∈ {0, . . . , |σ| -1}

• σ i = σ ′ i . When σ ′ ∈ E * , we note σ σ ′ def = σ ≺ σ ′ ∨ σ = σ ′ . For σ ∈ E ∞ ,
we will need to designate its subsequences. Execution sequences. A program P is considered as a generator of execution sequences. We are interested in a restricted set of operations the program can perform. These operations influence the truth value of properties the program is supposed to fulfill. We abstract these operations by a finite set of events, namely a vocabulary Σ. We denote by P Σ a program for which the vocabulary is Σ. The set of execution sequences of P Σ is denoted

Exec(P Σ ) ⊆ Σ ∞ . This set is prefix-closed, that is ∀σ ∈ Exec(P Σ ), σ ′ ∈ Σ * • σ ′ σ ⇒ σ ′ ∈ Exec(P Σ ).
Such execution sequences can be made of access events on a secure system to its ressources, or kernel operations on an operating system. In a software context, these events may be abstractions of relevant instructions such as variable modifications or procedure calls.

Properties

Properties as sets of of execution sequences. In this paper we aim to enforce properties on program. A property ϕ is defined as a set of execution sequences, i.e. ϕ ⊆ Σ ∞ . Considering a given execution sequence σ, when σ ∈ ϕ (noted ϕ(σ)), we say that σ satisfies ϕ. A consequence of this definition is that properties we will consider are restricted to single execution sequences, excluding specific properties defined on powersets of execution sequences.

Reasonable properties. As noticed in [START_REF] Ligatti | Runtime Enforcement of Nonsafety Policies[END_REF], a property can be effectively enforced at runtime only if it is reasonable in the following sense: it should be satisfied by the empty sequence, and it should be decidable.This means that a program which performs no action should not violate this property, and that deciding whether any finite execution sequence satisfies or not this property should be a computable function ([3]).

A Safety-Progress classification of properties

This section recalls and extends some results about the safety-progress [START_REF] Chang | The safety-progress classification[END_REF][START_REF] Chang | Characterization of temporal property classes[END_REF][START_REF] Manna | A hierarchy of temporal properties[END_REF] classification of properties. In the original papers this classification introduced a hierarchy between properties defined as infinite execution sequences. We extend here this classification to deal also with finite-length execution sequences.

Generalities about the classification

The safety-progress classification is constituted of four basic classes defined over infinite execution sequences:

safety properties are the properties for which whenever a sequence satisfies a property, all its prefixes satisfy this property. -guarantee properties are the properties for which whenever a sequence satisfies a property, there are some prefixes (at least one) satisfying this property. -response properties are the properties for which whenever a sequence satisfies a property, an infinite number of its prefixes satisfy this property. -persistence properties are the properties for which whenever a sequence satisfies a property, all its prefixes continuously satisfy this property from a certain point.

Furthermore, two extra classes can be defined as (finite) boolean combinations of basic classes.

-The obligation class is the class obtained by positive boolean combinations of safety and guarantee properties. -The reactivity class is the class obtained by boolean combinations of response and persistence properties.

Example 1. Let consider an operating system where a given operation op is allowed only when an authorization auth has been granted before. Then, -the property ϕ 1 stating that "an authorization grant grant auth should precede any occurrence of op" is a safety property; -the property ϕ 2 stating that "the next authorization request req auth should be eventually followed by a grant (grant auth) or a deny (deny auth)" is a guarantee property; -the property ϕ 3 stating that "the system should run forever, unless a deny auth is issued, meaning that every user should be disconnected and the system should terminate" is an obligation property;

the property ϕ 4 stating that "each occurrence of req auth should be first written in a log file and then answered either with a grant auth or a deny auth without any occurrence of op in the meantime" is a response property; -the property ϕ 5 stating that "an incorrect use of operation op should imply that any future call to req auth will always result in a deny auth answer" is a persistence property.

The safety-progress classification is an alternative to the more classical safetyliveness [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF][START_REF] Alpern | Defining liveness[END_REF] dichotomy. Unlike this later, the safety-progress classification is a hierarchy and not a partition. It provides a finer-grain classification, and the properties of each class can be characterized according to four views [START_REF] Chang | The safety-progress classification[END_REF]. We shall consider here only the so-called automata view.

The automata view

First, we define a notion of property recognizer using a variant of deterministic and complete Streett automata (introduced in [START_REF] Streett | Propositional dynamic logic of looping and converse[END_REF] and used in [START_REF] Chang | The safety-progress classification[END_REF]).

Definition 1 (Streett automaton).

A deterministic Streett automaton is a tuple (Q, q init , Σ, -→, {(R 1 , P 1 ), . . . , (R m , P m )}) defined relatively to a set of events Σ. The set Q is the set of automaton states, where q init ∈ Q is the initial state. The total function -→: Q × Σ → Q is the transition function. In the following, for q, q ′ ∈ Q, e ∈ Σ we abbreviate -→ (q, e) = q ′ by q e -→ q ′ . The set {(R 1 , P 1 ), . . . , (R m , P m )} is the set of accepting pairs, in which for all i ≤ n, R i ⊆ Q are the sets of recurrent states, and P i ⊆ Q are the sets of persistent states.

We refer an automaton with m accepting pairs as a m-automaton. When m = 1, a 1-automaton is also called a plain-automaton, and we refer R 1 and P 1 as R and P . In the following (otherwise mentioned) σ ∈ Σ ω designates an execution sequence of a program, and

A = (Q A , q init A , Σ, -→ A , {(R 1 , P 1 ), . . . , (R m , P m )}) a deterministic Streett m-automaton.
The run of σ on A is the sequence of states involved by the execution of σ on A. It is formally defined as run(σ, A)

= q 0 • q 1 • • • where ∀i • (q i ∈ Q A ∧ q i σi -→ A q i+1 ) ∧ q 0 = q init
A . The trace resulting in the execution of σ on A is the unique sequence (finite or not) of tuples (q 0 , σ 0 , q 1 ) • (q 1 , σ 1 , q 2 ) • • • where run(σ, A) = q 0 • q 1 • • • . We denote by vinf (σ, A) (or vinf (σ) when clear from context) the set of states appearing infinitely often in run(σ, A). This set is formally defined as follows:

vinf (σ, A) = {q ∈ Q A | ∀n ∈ N, ∃m ∈ N • m > n ∧ q = q m with run(σ, A) = q 0 • q 1 • • • .
The following definition tells whether an execution sequence is accepted or not by a Streett automaton: Definition 2 (Acceptance condition of a Street automaton). For an infinite execution sequence σ ∈ Σ ω , we say that

A accepts σ if ∀i ∈ {1, . . . , m} • vinf (σ, A) ∩ R i = ∅ ∨ vinf (σ, A) ⊆ P i .
For a finite execution sequence σ ∈ Σ * such that |σ| = n, we say that the m-automaton A accepts σ if either σ = ǫ or (∃q 0 , . . . , q n ∈ Q

A • run(σ, A) = q 0 • • • q n ∧ q 0 = q init
A and ∀i ∈ {1, . . . , m}

• q n ∈ P i ∪ R i ).
Note that this definition of acceptance condition for finite sequences matches the definition of finitary properties defined in [START_REF] Chang | The safety-progress classification[END_REF] (see [START_REF] Falcone | Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties[END_REF] for more details).

The hierarchy of automata. Each class of the safety-progress classification is characterized by setting syntactic restrictions on a deterministic Streett automaton.

-A safety automaton is a plain automaton such that R = ∅ and there is no transition from a state q ∈ P to a state q ′ ∈ P . -A guarantee automaton is a plain automaton such that P = ∅ and there is no transition from a state q ∈ R to a state q ′ ∈ R. -An m-obligation automaton is an m-automaton such that for each i in {1, . . . , m}:

• there is no transition from q ∈ P i to q ′ ∈ P i ,

• there is no transition from q ∈ R i to q ′ ∈ R i , -A response automaton is a plain automaton such that P = ∅ -A persistence automaton is a plain automaton such that R = ∅.

-A m-reactivity automaton is any unrestricted m-automaton.

Automata and properties. We say that a Streett automaton A ϕ defines a property ϕ (defined as a subset of Σ ∞ ) if and only if the set of execution sequences accepted by A ϕ is equal to ϕ. Conversely, a property ϕ ⊆ Σ ∞ is said to be specifiable by an automaton if the set of execution sequences accepted by the automaton is ϕ. A property ϕ that is specifiable by an automaton is a κ-property iff the automaton is a κ-automaton, where κ ∈ {safety, guarantee, obligation, response, persistence, reactivity}. In the following we note Safety(Σ) (resp. Guarantee(Σ), Obligation(Σ), Response(Σ), Persistence(Σ), Reactivity(Σ)) the set of safety (resp. guarantee, obligation, response, persistence, reactivity) properties defined over Σ.

Property enforcement via enforcement monitors

A program P is considered as a generator of execution sequences. We want to build an enforcement monitor (EM) for a property ϕ such that the two following constraints hold: soundness: any execution sequence allowed by the EM should satisfy ϕ; transparency: execution sequences of P should be modified in a minimal way, namely if a sequence already satisfies ϕ it should remain unchanged, otherwise its longest prefix satisfying ϕ should be allowed by the EM.

Enforcement monitors

We define now the central notion of enforcement monitor. Such a runtime device monitors a target program by observing relevant events and performing some enforcement operation depending on its internal state.

Definition 3 (Enforcement monitor (EM)). An enforcement monitor A ↓ is a 4-tuple (Q A ↓ , q init A ↓ , Stop A ↓ , -→ A ↓ ) defined relatively to a set of events Σ and a set of enforcement operations Ops. The finite set Q A ↓ denotes the control states,

q init A ↓ ∈ Q A ↓ is the initial state and Stop A ↓ is the set of stopping states (Stop A ↓ ⊆ Q A ↓ ). The partial function (but complete wrt. Q A ↓ × Σ) -→ A ↓ : Q A ↓ × Σ × Ops → Q A ↓
is the transition function. In the following we abbreviate -→ A ↓ (q, a, α) = q ′ by q a/α -→ A ↓ q ′ . We also assume that outgoing transitions from a stopping state only lead to another stopping state:

∀q ∈ Stop A ↓ • ∀a ∈ Σ • ∀α ∈ Ops • ∀q ′ ∈ Q A ↓ • q a/α -→ A ↓ q ′ ⇒ q ′ ∈ Stop A ↓ .
Notions of run and trace (see Sect. 3.2) are naturally transposed from Streett automata. In the remainder of this section, σ ∈ Σ ∞ designates an execution sequence of a program, and

A ↓ = (Q A ↓ , q init A ↓ , Stop A ↓ , -→ A ↓ ) designates an EM.
Typical enforcement operations allow the EM either to halt the target program (when the current input sequence irreparably violates the property), or to store the current event in a memory device (when a decision has to be postponed), or to dump the content of the memory device (when the target program comes back to a correct behavior). We first give a more precise definition of such enforcement operations, then we formalize the way an EM reacts to an input sequence provided by a target program through the standard notions of configuration and derivation.

Definition 4 (Enforcement operations Ops). Enforcement operations take as inputs an event and a memory content (i.e., a sequence of events) to produce a new memory content and an output sequence: Ops ⊆ 2 ((Σ∪{ǫ})×Σ * )→(Σ * ×Σ * ) . In the following we consider a set Ops = {halt, store, dump} defined as follows:

∀a ∈ Σ ∪ {ǫ}, ∀m • Σ * halt(a, m) = (ǫ, m) store(a, m) = (ǫ, m.a) dump(a, m) = (m.a, ǫ)
In the following we assume that outgoing transitions from a stopping state are all labeled with an halt operation. That is:

∀q ∈ Stop A ↓ • ∀a ∈ Σ • ∀α ∈ Ops • ∀q ′ ∈ Q A ↓ • q a/α -→ A ↓ q ′ ⇒ α = halt.

Definition 5 (EM configurations and derivations). For an EM

A ↓ = (Q A ↓ , q init A ↓ , Stop A ↓ , -→ A ↓ ), a configuration is a triplet (q, σ, m) ∈ Q A ↓ × Σ * × Σ *
where q denotes the current control state, σ the current input sequence, and m the current memory content.

We say that a configuration (q ′ , σ ′ , m ′ ) is derivable in one step from the configuration (q, σ, m) and produces the output o ∈ Σ * , and we note (q, σ, m)

o ֒→ (q ′ , σ ′ , m ′ ) if and only if σ = a.σ ′ ∧ q a/α -→ A ↓ q ′ ∧ α(a, m) = (o, m ′ ).
We say that a configuration C ′ is derivable in several steps from a configuration C and produces the output o ∈ Σ * , and we note C o =⇒ A ↓ C ′ , if and only if there exits k ≥ 0 and configurations

C 0 , C 1 , . . . , C k such that C = C 0 , C ′ = C k , C i oi ֒→ C i+1 for all 0 ≤ i < k, and o = o 0 • o 1 • • • o k-1 .
Besides, the configuration C is derivable from itself in one step and produces the output ǫ, we note C ǫ ⇒ C.

Enforcing a property

We now describe how an EM can enforce a property on a given program, namely how it transforms an input sequence σ into an output sequence o by performing derivation steps from its initial state. For the upcoming definitions we will distinguish between finite and infinite sequences and we consider an EM

A ↓ = (Q A ↓ , q init A ↓ , Stop A ↓ , -→ A ↓ ).
Definition 6 (Sequence transformation). We say that:

-The sequence σ ∈ Σ * is transformed by A ↓ into the sequence o ∈ Σ * , which is noted (q init A ↓ , σ) ⇓ A ↓ o, if ∃q ∈ Q A ↓ , m ∈ Σ * such that (q init A ↓ , σ, ǫ) o =⇒ A ↓ (q, ǫ, m). -The sequence σ ∈ Σ ω is transformed by A ↓ into the sequence o ∈ Σ ∞ , which is noted (q init A ↓ , σ) ⇓ A ↓ o, if ∀σ ′ ∈ Σ * • σ ′ ≺ σ • (∃o ′ ∈ Σ * • (q init A ↓ , σ ′ ) ⇓ A ↓ o ′ ∧ o ′ o).
Definition 7 (Property-Enforcement). Let consider a property ϕ, we say that A ↓ enforces the property ϕ on a program P Σ (noted Enf (A ↓ , ϕ, P Σ )) iff -∀σ ∈ Exec(P Σ ) ∩ Σ * , ∃o ∈ Σ * • enforced (σ, o, A ↓ , ϕ), where the predicate enforced (σ, o, A ↓ , ϕ) is the conjonction of the following constraints:

(q init A ↓ , σ) ⇓ A ↓ o (1) ϕ(o) (2) ϕ(σ) ⇒ σ = o (3) ¬ϕ(σ) ⇒ ∃σ ′ ≺ σ • ϕ(σ ′ ) ∧ o = σ ′ ∧ ∃σ ′′ ≻ σ ′ • ϕ(σ ′′ ) ∧ σ ′′ σ (4) -∀σ ′ ∈ Exec(P Σ ) ∩ Σ ω , ∀σ ≺ σ ′ , ∃o ∈ Σ * • enforced (σ, o, A ↓ , ϕ).
(1) stipulates that the sequence σ is transformed by A ↓ into a sequence o, (2) states that o satisfies the property ϕ, (3) ensures transparency of A ↓ , i.e. if σ satisfied already the property then it is not transformed, and (4) ensures in the case where σ does not satisfy ϕ that o is the longest prefix of σ satisfying the property.

Example 2 (Enforcement monitor). We provide on Fig. 1 two EMs to illustrate the enforcement of some of the properties introduced in example 1. We assume here that the set Σ of relevant events is {op, grant auth} (other events are ignored by the EM). A ↓ϕ1 has one stopping state, Stop = {2}, and its initial state is 1. From this initial state it simply dumps a first occurrence of grant auth and moves to state 3, where all events of Σ are allowed (i.e., dumped). Otherwise, if event op occurs first, then it moves to state 2 and halts the underlying program forever. -The right-hand side of Fig. 1 is an EM A ↓ϕ2 for the guarantee property ϕ 2 . We assume here that the set Σ of relevant events is {req auth, grant auth, deny auth}. The initial state of A ↓ϕ2 is state 1, and it has no stopping states. Its behavior is the following: occurrences of req auth are stored in memory as long as grant auth or deny auth does not occur, then the whole memory content is dumped. This ensures that the output sequence always satisfies the property under consideration.

Enforcement wrt. the safety-progress classification

We now study how to practically enforce properties of the safety-progress hierarchy (Sect. 3). More precisely, we show which classes of properties can be effectively enforced by an EM, and more important, we provide a systematic construction of an EM enforcing a property ϕ from the Streett automaton defining this property. This construction technique is specific to each class of properties.

From a recognizing automaton to an enforcement monitor

We define four general operations those purpose is to transform a Streett automaton recognizing a safety (resp. guarantee, obligation, response) property into an enforcement monitor enforcing the same property.

Definition 8 (Safety Transformation). Given a Streett safety-automaton

A ϕ = (Q Aϕ , q init Aϕ , Σ, -→ Aϕ , (∅, P )) recognizing a reasonable safety property ϕ defined over a language Σ, we define a transformation (named

TransSafety) of this automaton into an enforcement monitor

A ↓ϕ = (Q A ↓ϕ , q init A ↓ϕ , Stop A ↓ϕ , -→ A ↓ϕ ) such that: -Q A ↓ϕ = Q Aϕ , q init A ↓ϕ = q init
Aϕ , with q init Aϕ ∈ P -Stop A ↓ϕ = P the transition relation → A ↓ϕ is defined from -→ Aϕ as the smallest relation verifying the following rules:

• q a/dump -→ A ↓ϕ q ′ if q ′ ∈ P ∧ q a -→ Aϕ q ′ • q a/halt -→ A ↓ϕ q ′ if q ′ / ∈ P ∧ q a -→ Aϕ q ′
Note that there is no transition (in the Streett automaton) from q / ∈ P to q ′ ∈ P , and R = ∅. We note A ↓ϕ = TransSafety(A ϕ ).

Informally, the behavior of an EM A ↓ϕ obtained from TransSafety(A ϕ ) can be understood as follows. While the current execution sequence satisfies the underlying property (i.e while A ϕ remains in P -states), it dumps each input event. Once the execution sequence deviates from the property (i.e., when A ϕ reaches a P -state), then it halts immediately the underlying program with a halt operation. The following example illustrates this principle.

Example 3 (Safety Transformation). Fig. 2 (left-hand side) depicts a Streett automaton defining the safety property ϕ 1 of example 1. Its set of states is {1, 2, 3}, the initial state is 1, and we have R = ∅ and P = {1, 3}. The right-hand side shows the corresponding EM obtained using transformation TransSafety.

We now define a similar transformation for guarantee properties. The TransGuarantee transformation uses the set Reach Aϕ (q) of reachable states from a state q. Given a Street automaton A ϕ with a set of states Q Aϕ , we have

∀q ∈ Q Aϕ • Reach Aϕ (q) = {q ′ ∈ Q Aϕ | ∃(q i ) i , (a i ) i , •q a0 -→ Aϕ q 0 a1 -→ Aϕ q 1 • • • q ′ }.

Definition 9 (Guarantee Transformation). Let consider a Streett guarantee-automaton

A ϕ = (Q Aϕ , q init
Aϕ , Σ, -→ Aϕ , (R, ∅)) recognizing a property ϕ ∈ Guarantee(Σ). We define a transformation TransGuarantee of this automaton into an EM A ↓ϕ = (Q A ↓ϕ , q init A ↓ϕ , Stop A ↓ϕ , -→ A ↓ϕ ) such that:

-Q A ↓ϕ = Q Aϕ , q init A ↓ϕ = q init Aϕ , -Stop A ↓ϕ = {q ∈ Q A ↓ϕ | ∃q ′ ∈ Reach Aϕ (q) ∧ q ′ ∈ R} -the transition relation → A ↓ϕ is defined from -→ Aϕ as the smallest relation
verifying the following rules:

• q a/dump -→ A ↓ϕ q ′ if q ′ ∈ R ∧ q a -→ Aϕ q ′ • q a/halt -→ A ↓ϕ q ′ if q ′ / ∈ R ∧ q a -→ Aϕ q ′ ∧ ∃q ′′ ∈ R • q ′′ ∈ Reach Aϕ (q ′ ) • q a/store -→ A ↓ϕ q ′ if q ′ / ∈ R ∧ q a -→ Aϕ q ′ ∧ ∃q ′′ ∈ R • q ′′ ∈ Reach Aϕ (q ′ )
Note that there is no transition from q ∈ R to q ′ ∈ R. And, as P = ∅, we do not have transition from q ∈ P to q ′ ∈ P . We note A ↓ϕ = TransGuarantee(A ϕ ).

An EM A ↓ϕ obtained from TransGuarantee(A ϕ ) behaves as follows. While the current execution sequence does not satisfy the underlying property (i.e., while A ϕ remains in R-states), it stores each entered event in its memory. Once, the execution sequence satisfies the property (i.e., when A ϕ reaches an R-state), it dumps the content of the memory and the current event. The following example illustrates this principle.

Example 4 (Guarantee Transformation). Fig. 3 (up) shows a Streett automaton recognizing the guarantee property ϕ 2 of example 1. Its set of states is {1, 2}, the initial state is 1, and we have R = {2} and P = ∅. At the bottom is depicted the EM enforcing this same property, obtained by the TransGuarantee transformation. One can notice that this EM has no stopping state.

We now define a transformation for obligation properties. Informally the TransObligation transformation combines the effects of the two previously introduced transformations on using information of each accepting pair.

Definition 10 (Obligation Transformation). Let consider a Streett obligation-automaton

A ϕ = (Q Aϕ , q init
Aϕ , Σ, -→ Aϕ , {(R 1 , P 1 ), . . . , (R m , P m )}) recognizing an obligation property ϕ ∈ Obligation(Σ) defined over a language Σ. We define a transformation TransObligation of this automaton into an EM A ↓ϕ = (Q A ↓ϕ , q init A ↓ϕ , Stop A ↓ϕ , -→ A ↓ϕ ) such that:

-Q A ↓ϕ = Q Aϕ , q init A ↓ϕ = q init Aϕ , -Stop A ↓ϕ = m i=1 (P i {q ∈ Q A ↓ϕ | ∃q ′ ∈ Reach Aϕ (q) ∧ q ′ ∈ R i })
the transition relation → A ↓ϕ is defined from -→ Aϕ as the smallest relation verifying the following rule:

q a/α -→ A ↓ϕ q ′ if q a -→ Aϕ q ′ and α = ⊓ m i=1 (⊔(β i , γ i ))
where • ⊓, ⊔ designate respectively the infimum and the supremum with respect to the complete lattice (Ops, ⊑), where halt ⊑ store ⊑ dump (⊑ is a total order), • and the β i and γ i are obtained in the following way:

* β i = dump if q ′ ∈ P i * β i = halt if q ′ / ∈ P i * γ i = dump if q ′ ∈ R i * γ i = halt if q ′ / ∈ R i ∧ ∃q ′′ ∈ R i • q ′′ ∈ Reach Aϕ (q ′ ) * γ i = store if q ′ / ∈ R i ∧ ∃q ′′ ∈ R i • q ′′ ∈ Reach Aϕ (q ′ )
Note that there is no transition from q ∈ R i to q ′ ∈ R i , and no transition from q ∈ P i to q ′ ∈ P i .

Finding a transformation for a response property ϕ needs to slightly extend the definition of TransGuarantee to deal with transitions of a Streett automaton leading from states belonging to R to states belonging to R (since such transitions are absent when ϕ is a guarantee property). Therefore, we introduce a new transformation called TransResponse obtained from the TransGuarantee transformation (Def. 9) by adding a rule to deal with the aforementioned difference.

Definition 11 (Response Transformation). Let consider a Streett responseautomaton

A ϕ = (Q Aϕ , q init
Aϕ , Σ, -→ Aϕ , (R, ∅)) recognizing a response property ϕ ∈ Response(Σ) defined over a language Σ. We define a transformation TransResponse of this automaton into an enforcement monitor A ↓ϕ = (Q A ↓ϕ , q init A ↓ϕ , Stop A ↓ϕ , -→ A ↓ϕ ) using the transformations of the TransResponse transformation and adding the following rules to define → A ↓ϕ from → Aϕ :

q a/store -→ A ↓ϕ q ′ if q ∈ R ∧ q ′ / ∈ R ∧ q a -→ Aϕ q ′ ∧ ∃q ′′ ∈ R • q ′′ ∈ Reach Aϕ (q ′ ) q a/halt -→ A ↓ϕ q ′ if q ∈ R ∧ q ′ / ∈ R ∧ q a -→ Aϕ q ′ ∧ ∃q ′′ ∈ R • q ′′ ∈ Reach Aϕ (q ′ )
An EM A ↓ϕ obtained from TransGuarantee(A ϕ ) behaves as follows. Informally the principle is similar to the one of guarantee enforcement, except that there might be an alternation in the run between states of R and R. While the current execution sequence does not satisfy the underlying property (the current state of A ϕ is in R), it stores each event of the input sequence. Once, the execution sequence satisfies the property (the current state of A ϕ is in R), it dumps the content of the memory and the current event.

Example 5 (Response Transformation). Fig. 4 (left-hand side) shows a Streett automaton recognizing the response property ϕ 4 introduced in example 1. Its set of states is {1, 2, 3, 4}, the initial state is 1, and we have R = {1} and P = ∅. The right-hand side shows the EM enforcement the same property, obtained by the TransResponse transformation. One can notice there is one stopping state 4. Using the aforementioned transformations it is possible to derive an EM of a certain property from a recognizing automaton for this (enforceable) property.

In the following, we characterize the set of enforceable properties wrt. the safetyprogress classification.

Enforceable properties. Now, we delineate the class of enforceable properties. Notably, the safety (resp. guarantee, obligation and response) properties are enforceable. Given any safety (resp. guarantee, obligation, response) property ϕ, and a Streett automaton recognizing ϕ, one can synthesize from this automaton an enforcing monitor for ϕ using systematic transformations. This also proves the correctness of these transformations.

Theorem 1. Given a program P Σ , a reasonable safety (resp. guarantee, obligation, response) property ϕ ∈ Safety(Σ) (resp. ϕ ∈ Guarantee(Σ), ϕ ∈ Obligation(Σ), ϕ ∈ Response(Σ)) is enforceable on P(Σ) by an EM obtained by the application of the safety (resp. guarantee, obligation, response) transformation on the automaton recognizing ϕ. More formally, given A ϕ recognizing ϕ, we have:

(ϕ ∈ Safety(Σ) ∧ A ↓ϕ = TransSafety(A ϕ )) ⇒ Enf (A ↓ϕ , ϕ, P Σ ), (ϕ ∈ Guarantee(Σ) ∧ A ↓ϕ = TransGuarantee(A ϕ )) ⇒ Enf (A ↓ϕ , ϕ, P Σ ). (ϕ ∈ Obligation(Σ) ∧ A ↓ϕ = TransObligation(A ϕ )) ⇒ Enf (A ↓ϕ , ϕ, P Σ ). (ϕ ∈ Response(Σ) ∧ A ↓ϕ = TransResponse(A ϕ )) ⇒ Enf (A ↓ϕ , ϕ, P Σ ).
Complete proofs for each class of properties are provided in [START_REF] Falcone | Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties[END_REF].

Non-enforceable properties. Persistence properties are not enforceable by our enforcement monitors. Such a property is ϕ 5 introduced in example 1 stating that "an incorrect use of operation op should imply that any future call to req auth will always result in a deny auth answer". One can understand the enforcement limitation intuitively using the following argument: if this property was enforceable it would imply that an enforcement monitor could decide from a certain point that the underlying program will always produce the event deny auth in response to a req auth. However such a decision can never be taken without reading and memorizing first the entire execution sequence. This is of course unrealistic for an infinite sequence. As a straightforward consequence, properties of the reactivity class (containing the persistence class) are not enforceable by our enforcement monitors.

Discussion

An important question not yet addressed in this paper concerns the practical issues and possible limitations raised by the approach we propose. These limitations fall in several categories.

First, it is likely the case that not all events produced by an underlying program could be freely observed, suppressed, or inserted. This leads to wellknown notions of observable and/or controllable events, that have to be taken into account by the enforcement mechanisms. To illustrate such a limitation, consider a system in which there is a data-flow dependence between two actions. It seems in this case that the enforcement ability is impacted since the first action cannot be frozen (otherwise, the second action could not be executed). Another example is that some actions, important from the security point of view, may not be visible from outside the system (and hence from any enforcement mechanism). Solving these kinds of issues means either further refining the class of enforceable properties (taking these limitations into account), or being able to replace non-controllable or non-observable actions by "equivalent" ones.

Moreover, it could be also necessary to limit the memory resources consumed by the monitor. A possible solution is to store only an abstraction of the sequence of events observed (e.g. using a bag instead of a FIFO queue, or a set as in [START_REF] Fong | Access control by tracking shallow execution history[END_REF]). From a theoretical point of view, this means defining enforcement up to some abstraction preserving trace equivalence relations. We strongly believe that our notion of enforcement monitors (with a generic memory device) is a suitable framework to study and implement this feature.

Furthermore, an other working direction concerns confidence indebted to the implementation of such enforcement monitors. Such an implementation should remain in a size which permits to prove the adequacy between the enforced property and the semantics of the original underlying program. Such a concern follows the well-known principle of minimizing the trusted computing base.

Conclusion

In this paper our purpose was to extend in several directions previous works on security checking through runtime enforcement. Firstly, we proposed a generic notion of finite-state enforcement monitors based on generic memory device and enforcement operations. Moreover, we specified their enforcement abilities wrt. the general safety-progress classification of properties. It allowed a fine-grain characterization of the space of enforceable properties, which encompasses previous results on this area. Finally, we proposed a set of (simple) transformations to produce an enforcement monitor from the Streett automaton recognizing a given safety, guarantee, obligation or response security property. This feature is particularly appealing, since it allows to automatically generate enforcement monitors from high-level property definitions, like property specification patterns [START_REF] Dwyer | Property specification patterns for finite-state verification[END_REF] commonly used in system verification.

Several perspectives can be foreseen from this work, but the most important issue would be certainly to better demonstrate its practicability, as discussed in Sect. 6. A prototype tool is currently under development, and we plan to evaluate it on relevant case studies in a near future.

Fig. 1 .

 1 Fig. 1. Two examples of EMs

1 Fig. 2 .

 12 Fig. 2. Recognizing automaton and EM for the safety property ϕ1

↓ϕ 2 2 Fig. 3 .

 223 Fig.3. A guarantee-automaton and the corresponding EM for property ϕ2

Fig. 4 .

 4 Fig. 4. A response-automaton and the corresponding EM for property ϕ4