********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle S16, etage -1 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 14 octobre 2005 **************************************** Marco Pistoia (IBM Thomas J. Watson Research Center, Yorktown Heights, NY) Using Static Program Analysis for Stack-Inspection- and Role-Based Access Control Systems Security Abstract: With the advent of the Internet, downloading software components from untrusted sources has become a very common practice. Guaranteeing that the security of a system is not compromised by untrusted components is essential to preserve integrity and privacy. This talk presents an interprocedural analysis framework for statically representing the execution of software programs and the flow of security information in those programs. The results of the analysis can be used to automatically identify security properties of software and evaluate security policies. The interprocedural analysis can be applied to both Stack-Based Access Control (SIBAC) systems, such as Java 2, Standard Edition (J2SE) and Microsoft .NET Common Language Runtime (CLR), and Role-Based Access Control (RBAC) systems, such as Java 2, Enterprise Edition (J2EE) and CLR. In a SIBAC system, when there is a request to access a restricted resource, the access control mechanism checks if all the callers on the stack have the necessary permissions to access that resource. Permissions can be granted to code or subjects (users). A special function can be called to execute code under the authority of an authenticated subject. Sometimes, library code is programmed to access a restricted resource (for example, a configuration file) without explicit requests from its client. Since the client will be on the call stack when that resource is accessed, the client will need to be granted access to that resource as well, or an authorization failure will occur at run time. To avoid granting the client a permission that it does not explicitly need, which would be a violation of the "Principle of Least Privilege," a SIBAC system allows marking a portion of library code as "privileged." At run time, when privileged code is encountered, the stack traversal will stop at the library stack frame preceding the privileged code. As a result, all the remaining callers on the stack will be implicitly granted the permission to access the restricted resource. However, the untrusted client code could misuse its temporary permissions if it had a way to influence (or taint) the values of the variables used by the trusted library code in the privileged operations. This could lead to violations of the security policy and thus security breaches. In an RBAC system, access to resources is controlled through "security roles" rather than through the user identity. However, a user initiating a transaction must have been granted not just the roles necessary to invoke the transaction entry point, but all the roles needed to access each resource traversed by the transaction, taking into account that authorization checks are performed only when an access-restricted resource is accessed from another component. A "principal-delegation policy" can be used to override the roles granted on subsequent component calls. The interprocedural analysis framework presented in this talk can be used to automatically identify: Permissions and roles required by a program or library to run without authorization failures Portions of code that will be subject-executed Permissions obtained by code as a result of being executed by a subject Security problems generated by security policies that are too permissive Stability problems generated by security policies that are too restrictive Portions of library code that should be made privileged Presence of tainted variables in privileged code Permissions implicitly granted to client code by privileged library code Unnecessary or redundant privileged and subject-executed code Security inconsistencies generated by principal-delegation policies The analysis model presented in this talk has been implemented and used extensively to detect security vulnerabilities in large production-level programs. Parts of this work have been published at the OOPSLA 2002 and ECOOP 2005 conferences. *** Vendredi 28 octobre 2005 **************************************** Sarah Thompson (CPRG, Computer Laboratory, University of Cambridge, UK) An Abstract Interpretation-based Semantics for Radiation-Hard Asynchronous Circuits. Abstract: The effectiveness of program analysis techniques based upon sound mathematical abstract semantics has long been recognised. Though normally applied to software, this approach is also applicable to digital electronics. Most circuits are designed assuming a synchronous model; a single global clock signal drives the clock inputs of every flip flop in the system, and unclocked feedback loops are outlawed. This design approach works well, primarily because it makes circuits easy to reason about. The real world, however, is fundamentally asynchronous. Even something so simple as a push button exhibits the characteristic that it can change state at any time, requiring designers to be very careful when constructing appropriate interface circuits. Intuition based on the synchronous model tends to break down due to the need to consider timing information that is continuous in nature. Formal reasoning is generally difficult, so engineers often use inexact discrete time simulations that often miss possible pathological behaviour. Abstract interpretation provides a sound formal framework that allows abstractions of concrete systems to be reasoned about. In our SAS'04 paper, we introduced transitional logic, an abstract interpretation technique resembling a multi-valued logic that is capable of supporting reasoning about asynchronous behaviour of combinational circuits. In this talk, I will first present a gentle overview of transitional logic, then go on to show how it can be used to reason about the radiation hardness of majority voting circuits. Our analysis showed that, whilst permanent subsystem failure is tolerated as expected, brief single-event transients (SETs) of the kind typically caused by relativistic heavy ion (cosmic ray) impacts are not reliably rejected. This result can be generalised to show that, in general, delay-insensitive circuits are fundamentally incapable of rejecting SETs. (Joint work with Professor Alan Mycroft) ********************************************************************* Pour recevoir l'annonce par courrier electronique: WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************