Logo du LIFL

Depuis le 1er janvier 2015 le LIFL et le LAGIS forment le laboratoire CRIStAL

  1. Actualités

Séminaire de

Gurvan Le Guernic

3 février 2011
Amphi Turing, Bât M3

Monitoring & Compiling Safe Information Flows

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse security clearance. Security policies are specified by labeling inputs of outputs of programs. This approach allow to easily state security policies which can then often be verified statically or dynamic, or used to adapt a program in order to respect the stated policy.

 The first part of the talk presents briefly the main concepts behind  information flow monitoring. It introduces the notion of noninterference on which rely the majority of information flow analyses, and presents the main detection and correction mechanisms.

The second and main part of the talk presents a compiler to enforce information flow security policies in concrete distributed systems, which involves delicate compilation issues. We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract information-flow policy for accessing  the shared memory. In their implementations, shared memory is  unprotected and security depends instead on encryption and signing. We  build a translation from source programs with high-level security policies to cryptographic implementations. The translation enforces the correct usage of cryptographic primitives against active adversaries.


UMR 8022 - Laboratoire d'Informatique Fondamentale de Lille - Copyright © 2012 Sophie TISON - Crédits & Mentions légales

Page respectant XHTML et CSS.

Pour tout commentaire / Comments and remarks : webmaster