Colibri 09 presentations

Below you may find the slides for the talks I have given at the Colibri colloquium:

Automating model-based software engineering
David Déharbe (UFRN), Pascal Fontaine (LORIA), Stephan Merz (LORIA), Anamaria Martins Moreira (UFRN), Anderson Santana de Oliveira (UFERSA)

Vérification automatique des systèmes à base de règles avec le narrowing stratégique
Anderson Santana de Oliveira (UFERSA), David Déharbe (UFRN), Pierre-Etienne Moreau (INRIA)

18th International Workshop on Functional and (Constraint) Logic Programming WFLP’09

I am part of the program commitee for WFLP 2009, the 18th International Workshop on Functional and (Constraint) Logic Programming, part of RDP’09 which will take place in Brasilia.

Novo concurso para Ciências da Computação na UFERSA

A Universidade Federal Rural do Semi-Árido, UFERSA, da qual faço parte hoje, abriu inscrições para 5 vagas para professor adjunto com dedicação exclusiva para o curso de Ciências da Computação. O requisito é formação em computação e áreas afins. O diploma de doutorado deve ser apresentado somente no ato da posse, portanto, se você está prestes a defender a tese, esta é uma excelente oportunidade. Um atrativo é o programa de mestrado em cooperação ampla com a Universidade do Estado do Rio Grande do Norte, UERN.

Confira o edital em: http://www.ufersa.edu.br/concursos/

Faculty Position at UFRN, Natal Brazil

The Federal University of Rio Grande do Norte has opened a permanent
Faculty Position in the area of “Integrated Circuits Design”.
Prospective candidates are invited to visit
“http://www.dimap.ufrn.br/concurso2008″ for details about the
application procedure. All information is in Portuguese as this is the
working language in our Institution.

We will be receiving application until November 7th, 2008. Gross
salary starts at BR$6.497,15.

Recent papers

I have participated in two papers that were presented at SecRet 2008:

• Claude Kirchner, Hélène Kirchner and Anderson Santana de Oliveira – Analysis of Rewrite-Based Access Control Policies
  

  The rewrite-based approach provides executable specifications for security policies, which can be independently designed, verified, and then anchored on programs using a modular discipline. In this paper, we describe how to perform queries over these rule-based policies in order to increase the trust of the policy author on the correct behavior of the policy. The analysis we provide is founded on the narrowing process, which provides both the necessary abstraction for simulating executions of the policy over access requests and the
  mechanism for solving what-if queries from the security administrator. We illustrate this general approach by the analysis of a firewall system policy.

• Horatiu Cirstea, Pierre-Etienne Moreau and Anderson Santana de Oliveira – Rewrite Based Specification of Access Control Policies
  

  Data protection within information systems is one of the main concerns in computer systems security and different access control policies can be used to specify the access requests that should be granted or denied. These access control mechanisms should guarantee that
  information can be accessed only by authorized users and thus prevent all information leakage. We propose a methodology for specifying and implementing access control policies using the rewrite based framework Tom. This approach allows us to check that any reachable state
  obtained following an access granted in the implementation satisfies the policy specification. We show that when security levels are not totally ordered some information leakage can be detected.

Phd Thesis

My thesis defense will be on March 31st, in LORIA. For more information about the thesis check  this page: http://andersonsantana.wordpress.com/thesis-manuscript/

FMSE’07 presentation slides

The file below contain the slides of my talk at the FMSE workshop.

• FMSE’07 slides

Phd opportunity in Nancy, France

We are looking for candidates for a phd on the following subject:

Specification and Verification of Access Control Policies

click on the link above for more information.

Weaving Rewrite-Based Access Control Policies

With Claude Kirchner, Hélène Kirchner, and Eric Ke Wang

Access control is a central issue among the overall security goals
of information systems. Despite of the existence of a vast
literature on the subject, it is still very hard to assure the
compliance of a large existing system to a given dynamic access
control policy.

Based on our previous work on formal islands, we provide in this
paper a systematic methodology to weave dynamic, formally specified
policies on existing applications using aspect-oriented programming.

To that end, access control policies are formalized using term
rewriting systems, allowing us to have an agile, modular,
and precise way to specify and to ensure their formal
termination.

These high-level descriptions are then weaved into the existing
code, in a manner that the resulting program implements a safe
reference monitor for the specified policy.

For developers, this provides a systematic process to enforce
dynamic policies in a modular and flexible way. Since policies are
independently specified and checked to be later weaved into various
different applications, the level of reuse is improved. We
implemented the approach on test cases with quite encouraging
results.

Weaving Rewrite-Based Access Control Policies

• Accepted at The 5th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code – FMSE’07

Automated Detection of Information Leakage in Access Control

with Charles Morisset

The prevention of information flow is an important concern in several
access control models. Even though this property is stated in the model
specification, it is not easy to verify it in the actual implementation of a
given security policy. In this paper we model-check rewrite-based
implementations of access control policies. We propose a general
algorithm that allows one to automatically identify information leakage.
We apply our approach to the well-known security model of
Bell and LaPadula and show that its generalization proposed by
McLean does not protect a system against information leakage.

Automated Detection of Information Leakage in Access Control

• Accepted at Security and Rewriting Techniques – SecReT’07