Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Which Security properties are Enforceable byMonitors?
byRaphaël Khoury
Laval University

19 April 2013by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Outline1

Introduction

2

First Stage: Delineating the Set of Enforceable Properties

3

Second Stage: Memory and Computability Constraints

4

Third Stage: Alternate definitions of Enforcement

5

Avenues for Future Research

6

Conclusion and referencesby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

General Framework

Outline1

Introduction

2

First Stage: Delineating the Set of Enforceable Properties

3

Second Stage: Memory and Computability Constraints

4

Third Stage: Alternate definitions of Enforcement

5

Avenues for Future Research

6

Conclusion and referencesby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

General Framework

General Framework
A system is modeled by a (possibly infinite) set of actions Σ.
An execution is a finite or infinite sequence of actions from Σ.
A security policies of interest are subsets of valid sequences P̂termed properties.
The monitor is an automaton that receives a sequence as
input, and outputs another sequence.
We let σ and τ range over possible executions, and A(σ)
denote the output of monitor A when its input is σ. We writeP̂(σ) to indicate that the sequence σ respects the security
policy P̂.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

General Framework

Framework and Review of the Literature

When can we consider that a monitor enforces a security Policy?
An effective enforcement paradigm must be based on the following
2 principles (from Ligatti et al.):Correction The output sequence is valid.
Transparency The semantics of a valid input sequence is preserved.
An equivalence relation between executions limits themonitor’s ability to transform sequences.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Model by Schneider
Model by Ligatti et al.

Outline1

Introduction

2

First Stage: Delineating the Set of Enforceable Properties

3

Second Stage: Memory and Computability Constraints

4

Third Stage: Alternate definitions of Enforcement

5

Avenues for Future Research

6

Conclusion and referencesby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Model by Schneider
Model by Ligatti et al.

Model by Schneider

According to Schneider, a monitor can be modeled by anautomaton which observes the execution of the target
program and aborts the execution to prevent a violation of the
security property from occurring.
The monitor can only consider the execution in progress.
It possesses no information about the possible future behaviorof the program
It can only react to a potential violation of the security policy
by aborting the execution

In this context, only safety properties are enforceable.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Model by Schneider
Model by Ligatti et al.

Automata representation of Monitors

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Model by Schneider
Model by Ligatti et al.

Model by Ligatti et al.
Ligatti et al. extend Schneider’s model along three axes:
According to the means available to the monitor to react to apossible violation;
According to the information at the disposal of the monitor
about the program’s possible behavior(non-uniform context);
According to its capacity to transform valid sequences into
equivalent sequences.

The set of policies enforceable by these mechanisms increases
in the non-uniform context.
More diverse reaction mechanisms can extend the range ofenforceable policies, but only if the monitor is equipped with asufficiently flexible equivalence relation.
by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Model by Schneider
Model by Ligatti et al.

Results-Precise nonuniform enforcement

Edit Automata

Supression Automata
Truncation
Automata

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Model by Schneider
Model by Ligatti et al.

Results-Effective Enforcement enforcement
Edit Automata

Truncation
Automata

Insertion
Automata

Supression
Automata

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Model by Schneider
Model by Ligatti et al.

The Edit Automaton and infinite sequences

In a subsequent study, Ligatti et al. define the set ofproperties enforceable by an edit automaton, using syntactic
equality as its equivalence relation.
This corresponds to the set of infinite renewal property. A
property is in this set if every valid sequence has infinitely
many valid prefixes, while every infinite invalid sequences has
only finitely many such prefixes. All properties over finite
sequences are in this set.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Model by Schneider
Model by Ligatti et al.

Results-Infinite Renewal
All Properties
Infinite Renewal
Safetyby Raphaël Khoury

Liveness

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Computability Constraints
Memory Constraints

Outline1

Introduction

2

First Stage: Delineating the Set of Enforceable Properties

3

Second Stage: Memory and Computability Constraints

4

Third Stage: Alternate definitions of Enforcement

5

Avenues for Future Research

6

Conclusion and referencesby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Computability Constraints
Memory Constraints

Kim et al.

Kim et al. observe that only a subset of safety properties aretruncation enforceable since there exists properties for which
the monitor cannot detect the violation.
A property P̂ is enforceable by a security automaton iff P̂ is asafety property and the set Σ∗ \{pref(Property )} is recursively
enumerable.
This is the class of co-recursively enumerable languages(coRE).

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Computability Constraints
Memory Constraints

Hamlen et al.
Hemlen et al. proceed to compare the enforcement power ofmonitors, static analysis and code rewriting and link them tocomputability classes.
Statically enforceable properties are those for which there
exists a total computable procedure that decides them. This
coincides with the the class of recursively decidable properties.
Code rewriting is equivalent to effective∼= enforcement, it
includes all recursively decidable properties except the empty
property does not correspond to any computability class.
The class of co-recursively enumerable languages is actually asuperset of the set of properties enforceable by monitors, since
in some cases, the monitor might be able to detect theviolation but unable to react.
by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Computability Constraints
Memory Constraints

Hamlen et al.

A better characterization of the properties enforceable bymonitors is the intersection of coRE and of the set ofproperties enforceable by rewriters.
Properties in this intersection exhibit a particular behavior
termed benevolence.
A property is benevolent if there exists a decision procedurethat rejects any invalid prefix of an invalid execution, but
accepts any valid prefix of a valid execution.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Hamlen et al. -Resultsby Raphaël Khoury

Computability Constraints
Memory Constraints

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Computability Constraints
Memory Constraints

Fong- The Shallow History Automaton
Fong considers monitors that only records the shallow history(i.e. the unordered set of security relevant events performedby the target program).
He proposes a monitor-based model, the shallow history
automaton (SHA), to study their enforcement power.
The set of SHA-enforceable properties is necessarily a strict
subset of safety properties, but it does include many
interesting real-life properties:
the Chinese Wall Policy
the Low-Water-Mark policy
the One-out-of-k authorization
the Assured Pipelines policyby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Computability Constraints
Memory Constraints

Talhi et al.- The Bounded History Automaton
Talhi et al. study the enforcement power of a monitor
operating with a memory of bounded size.
The propose two new models, the Bounded Security
Automata (BSA) and the by Bounded Edit Automata (BEA),
to study such monitors.
The set of properties enforceable by BSA and BEA are
naturally subsets to the set of properties enforceable by theirunrestricted counterparts.
The set of properties enforceable by bounded automata
increases monotonously as a larger memory is made available
to the monitor.
There exists a close connection between the set of properties
enforceable by BHA and a class of properties termed locallytestable properties.
by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Computability Constraints
Memory Constraints

Beauquier et al.- The finite Automaton

Beauquier et al. examine the set of properties enforceable bymonitors whose memory is finite but unbounded.
They focus on effective enforcement and on uniform systems
containing both finite and infinite sequences with = as theequivalence relation.
They find that the set of enforceable properties to beintermediate to those enforceable by the BEA and by the edit
automaton.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Outline1

Introduction

2

First Stage: Delineating the Set of Enforceable Properties

3

Second Stage: Memory and Computability Constraints

4

Third Stage: Alternate definitions of Enforcement

5

Avenues for Future Research

6

Conclusion and referencesby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Review of the LiteratureFirst idea: precise enforcement (from Schneider) Every action of avalid sequence must be output in lockstep. ∀σ ∈ Σ∞
P̂(A(σ))P̂(σ) ⇒ ∀i : A(σi )by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Review of the Literature

Second Idea: effective∼= enforcement (from Ligatti et al.) The
output must be equivalent if the input is valid. ∀σ ∈ Σ∞
1P̂(A(σ))2P̂(σ) ⇒ A(σ) ∼=σby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Solution 1: Iterative Enforcement
One possible solution is to tie the notion of enforcement to a
specific policy. Bielova et al. suggest the notion of iterative
enforcement for a class of policies called iterative policies:∀σ ∈ Σ∞1 P̂(σ) ⇒ A(σ) = σ
2 ∀σ ∈ Σ∗ : ¬P̂(σ) : ∃σ ′  σ : P̂(σ ′ ) ⇒ A(σ) = σ where σ isoothe longest valid prefix of σ
3 ∀σ ∈ Σ∗ : ¬P̂(σ) ∧ ∀σ ′  σ : ¬P̂(σ ′ ) : ∃σ ∈ Σ : σ =bσo ; σb σr ⇒ A(σ) = σo ; A(σr ) where σo is the longest valid
prefix of σ, and σb is the smallest sequence s.t. after deleting
it from σ, the resulting sequence is valid.
Informally, a monitor iteratively enforces by suppression an iterative
property P̂ iff every valid transaction is output and every invalidtransaction is suppressed.
by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Solution 2: Syntactic Constraints

We can limit the number of insertions and suppressions performedby the monitor when correcting an invalid sequence. Formally, thisis done by adding a predictability requirement to the definition of
enforcement.
Predictability: A enforcement mechanism is predictable if every
trace that is close to some valid trace is mapped intoa trace close to the same valid trace.
This distance between traces can be quantified using establishedmetrics such as the Levenshtein distance.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Solution 3: Corrective∼= Enforcement

1

The monitor should be both :required to output a valid sequence, andforbidden from altering the semantics of the input.

2

Valid behaviors present in an invalid input sequence should bepreserved, while minimal alterations are made to correct the
input sequence.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Corrective∼= Enforcement

1

Corrective∼= Enforcement

2

An abstraction captures essential properties of the input
sequence, which must be preserved, despite the monitor’stransformations.

3

These abstractions are grouped into equivalence classes.

4

The output must always be kept equivalent to the input.
∀σ ∈ Σ∞

5P̂(A(σ))σ∼= A(σ)by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

ExamplesExamples1

Transactional properties: The equivalence relation is themultiset of valid transactions present in a sequence.

2

Renewal Properties: Two sequences are equivalent if theyshare the same longest valid prefix, w.r.t. the property ofinterest.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Solution 4: Corrective⊑ Enforcement

It is often easier to organise execution sequences into a preorder.
The output must be higher or equal to the input w.r.t thepreorder. ∀σ ∈ Σ∞
1P̂(A(σ))2σ ⊑ A(σ)

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Corrective⊑ Enforcement

1

We use an abstraction function F to capture the property of
the input sequence which must be preserved throughout the
manipulations performed by the monitor.

2

We let ≤ stand for a preorder over the codomain of F, and ⊑stand for a corresponding preorder over the possible execution
sequences, s.t. for any two sequences σ, σ ′σ ⊑ σ ′ ⇔ F(σ) ≤ F(σ ′ ).

3

The monitor is only allowed to replace an invalid sequence σwith a valid sequence σ ′ if σ ⊑ σ ′ .

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Example - Transactional Properties
Corrective enforcement allows several different enforcement
possibilities.
1 We let the abstraction function F be the function valid (σ)
which abstracts the multiset of valid transactions from asequence.
2 Two sequences have the same abstraction if they share thesame multiset of valid transactions, regardless of theirordering or of the presence of invalid transactions.
3 σ ⊑ σ ′ indicates that valid(σ) ⊆ valid(σ ′ ).
4 This allows the monitor to either suppress invalid transactions
or replace them with alternative valid transactions.
5 To be correctively⊑ enforceable, the set of valid transactions
must meet a restriction termed unambiguity.
by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Review of the Literature
Bounded Enforcement
Syntactic Constraints
Semantic Constraints

Other Examples

I investigated other possible security policies :1

The Assured Pipeline Policy

2

The Chinese Wall Policy

3

General Availability

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Monitor certification
Monitoring and Abstraction
Redundancy and Diversity
Reactive Automaton
Transparency

Outline1

Introduction

2

First Stage: Delineating the Set of Enforceable Properties

3

Second Stage: Memory and Computability Constraints

4

Third Stage: Alternate definitions of Enforcement

5

Avenues for Future Research

6

Conclusion and referencesby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Monitor certification
Monitoring and Abstraction
Redundancy and Diversity
Reactive Automaton
Transparency

There still exists several interesting avenues for future
research:
1-Can we certify the transparency of a monitor’s enforcement?

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Monitor certification
Monitoring and Abstraction
Redundancy and Diversity
Reactive Automaton
Transparency

There still exists several interesting avenues for future
research:
2-Which properties are enforceable in the presence of trace
abstraction?

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Monitor certification
Monitoring and Abstraction
Redundancy and Diversity
Reactive Automaton
Transparency

There still exists several interesting avenues for future
research:
3-How can we evaluate the use of diversity and redundancy forsecurity?

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Monitor certification
Monitoring and Abstraction
Redundancy and Diversity
Reactive Automaton
Transparency

There still exists several interesting avenues for future
research:
4-Can the set of enforceable properties be refined in the context of
the reactive automaton model?

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Monitor certification
Monitoring and Abstraction
Redundancy and Diversity
Reactive Automaton
Transparency

There still exists several interesting avenues for future
research:
5-Can security properties be stated in such a way that they include
a transparency requirement?

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Outline1

Introduction

2

First Stage: Delineating the Set of Enforceable Properties

3

Second Stage: Memory and Computability Constraints

4

Third Stage: Alternate definitions of Enforcement

5

Avenues for Future Research

6

Conclusion and referencesby Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

1

H. Chabot R. Khoury and N. Tawbi, “Generating In-Line Monitors For
Rabin Automata”, 14th Nordic Conference on Secure IT Systems, Oslo,
Norvège (octobre 2009), Springer’s Lecture Notes In Computer Science(LNCS).

2

H. Chabot, R. Khoury and N. Tawbi, “Extending the Enforcement Powerof Truncation Monitors Using Static Analysis”, Computers & Security.

3

R. Khoury and N. Tawbi,“Using Equivalence Relations for Corrective
Enforcement of Security Policies”, 5th International Conference
Mathematical Methods, Models, and Architectures for Computer
Networks Security (MMM-ACNS-2010), St-Petersburg, Russia, Sept.
2010, Springer’s Lecture Notes In Computer Science (LNCS).

4

R. Khoury and N. Tawbi,“A Corrective Enforcement Framework for
Runtime Monitors”, 7th International Workshop on Formal Aspects ofSecurity & Trust (FAST2010) Pisa, Italy, Sept. 2010, Springer’s Lecture
Notes In Computer Science (LNCS).

5

R. Khoury and N. Tawbi,“Corrective Enforcement of Security Policies”,
ACM Transactions on Information and System Security 15(2)(2012).
by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

1

R. Khoury and N. Tawbi, “Corrective Enforcement: A new Paradigm ofSecurity Policy enforcement by Monitors” Submitted for publication.

2

R. Khoury and N. Tawbi,“Which Security Policies are Enforceable byRuntime Monitors? A Survey”, Computer Science Review, 6(1), pp.27-45(2012).

3

F. Lemay and R. Khoury and N.Tawbi “Optimized Inlining of Runtime
Monitors”, In proceedings of the 16th Nordic Conference on Secure IT
Systems (NORDSEC11), Tallinn, (Estonia), October 2011, Springer’s
Lecture Notes In Computer Science (LNCS) series.

by Raphaël Khoury

Introduction
First Stage: Delineating the Set of Enforceable Properties
Second Stage: Memory and Computability Constraints
Third Stage: Alternate definitions of Enforcement
Avenues for Future Research
Conclusion and references

Thank You

Questions?
by Raphaël Khoury