Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __                                  
			  / _`  _   /  /  o           
			 /   ) __) /  /  / /  / /\/| 
			(___/ (_/ (_ (_ / (__/ /   |  
                                                
			  I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                            Lundi 6 octobre, 10h30

                               ---------------
                               Benjamin Pierce
                               ---------------

                          University of Pennsylvania

         ===========================================================
         Micro-Policies: A Framework for Tag-Based Security Monitors
         ===========================================================

Current cybersecurity practice is inadequate to defend against the threats
faced by society. A host of vulnerabilities arise from the violation of
known—but not enforced—safety and security policies,including both high-level
programming models and critical invariants of low-level programs. Unlike
safety-critical physical systems (cars, airplanes, chemical processing
plants), present-day computers lack supervising safety interlocks to help
prevent catastrophic failures.

We argue that a rich and valuable set of low-level MICRO-POLICIES can be
enforced at the hardware instruction-set level to provide such safety
interlocks with modest performance impact. The enforcement of these
micro-policies provides more secure and robust macro-scale behavior for
computer systems. We describe ongoing work following on from the DARPA
CRASH/SAFE project (www.crash-safe.org <http://www.crash-safe.org>) to (1)
introduce an architecture for ISA-level micro-policy enforcement; (2) develop
a linguistic framework for formally defining micro-policies; (3) identify and
implement a diverse collection of useful micro-policies; (4) verify, through a
combination of rigorous testing and formal proof, that combinations of
hardware and software handlers correctly implement the desired policies and
that the policies imply specific high-level safety and security properties;
and (5) microarchitecture to provide hardware support with low performance
overhead and acceptable resource costs. Thus, emerging hardware capabilities
and advances in formal specification and verification combine to enable
engineering systems with strong security and safety properties.

*Bio*: Benjamin Pierce is Henry Salvatori Professor of Computer and
Information Science at the University of Pennsylvania. His research interests
include programming languages, type systems, language-based security,
computer-assisted formal verification, differential privacy, and
synchronization technologies. He is the author of the widely used graduate
textbooks /Types and Programming Languages/ and /Software Foundations/ and the
lead designer of the popular Unison file synchronizer.