Xavier Leroy
email: xavier.leroy@inria.fr

Computer security from a programming language and static analysis perspective (Extended abstract of invited lecture)

 is usually defined as ensuring integrity, confidentiality, and availability requirements even in the presence of a determined, malicious opponent. Sensitive data must be modified and consulted by authorized users only (integrity, confidentiality); moreover, the system should resist "denial of service" attacks that attempt to render it unusable (availability). In more colorful language, computer security has been described as "programming Satan's computer" [6]: the implementor must assume that every weakness that can be exploited will be.

.

Access control

Access control is the most basic and widespread security policy. An access control policy provides yes/no answers to the question "is this principal (user, program, role, . . . ) allowed to perform this operation (read, write, creation, deletion, . . . ) on this resource (file, network connection, database record, . . . )?". Access control is effective to ensure integrity, and can also ensure simple confidentiality properties.

Preventing direct access to a resource

Access control is performed by fragments of code (OS kernel, reference monitor, privileged library) that check that access to a logical resource (file, network

connection) is allowed before performing the operation on the underlying lowlevel resource (disk or network controller). Of course, access control is moot if the program can bypass this code and operate directly on the low-level resource.

The traditional answer to this issue relies on hardware-enforced mechanisms: the low-level resources can only be accessed while the processor is in supervisor mode, and switching from user mode to supervisor mode can only be performed through specific entry points that branch to the access control code. On the user side, resources are represented indirectly by "handles", e.g. indices into kernel tables. Hardware memory management prevents user code from accessing kernel data directly.

This model, while effective, is not always suitable. Sometimes, user-mode programs must be further partitioned into relatively trusted (Web browser) and completely untrusted (Web applets). Switching between user and supervisor modes can be expensive. The required hardware support may not be present, e.g. in small embedded devices.

An alternate, language-based approach executes all code within the same memory space, without hardware protections, but relies on strong typing to restrict direct access to sensitive resources. These resources are directly represented by pointers, but strong typing prevents these pointers from being forged, e.g. by guessing their addresses. Thus, the typing discipline of the language can be used to enforce security invariants on the resources. 1As a trivial example, if a resource is not reachable from the initial memory roots of a piece of code, memory safety, also called garbage collection safety, ensures that this code can never access this resource. As a less trivial example, two standard type-based encapsulation techniques can be used to provide controlled access to a resource: procedural encapsulation and type abstraction [START_REF] Leroy | Security properties of typed applets[END_REF].

-With procedural encapsulation, the resource is a free variable of a function closure, or a private field of an object, and only the closure or the object are given to the untrusted code. The latter, then, cannot fetch the resource pointers directly from the object or the closure (this would be ill-typed), and must call the function or a method of the object to operate on the resource; the code of the function or the method will then perform the required access checks before performing the operation. -With type abstraction, the resource pointer itself can be given to the untrusted code, but its type is made abstract, preventing the code from operating directly on it; to use the resource, the code must call one of the operations provided in the signature of the abstract type, and this code will then perform access checks as described before.

As outlined above, strong typing can be exploited to enforce access control. The remaining question, then, is how to enforce a strong typing discipline during execution of (untrusted) code. A simple approach is to perform type checks dynamically, during program execution. This can be achieved in many ways: direct interpretation of the program source (if available); compilation of the source with insertion of run-time checks; bytecode interpretation of virtual machine code such as the JVM [START_REF] Lindholm | The Java Virtual Machine Specification[END_REF]; just-in-time compilation of said virtual machine code; and instrumentation of precompiled machine code with additional checks (software fault isolation) [START_REF] Wahbe | Efficient software-based fault isolation[END_REF].

To reduce the run-time overhead of dynamic type checking, it is desirable to perform some of the type checks statically, during a program analysis pass prior to actual execution. Static typing of source code is common and well understood [START_REF] Cardelli | Type systems[END_REF]. However, source for untrusted code is not always available. Moreover, bugs in the source-to-executable compiler could introduce type violations after type checking; in other terms, the compiler is part of the trusted computing base. These drawbacks can be avoided by performing static type-checking on lowerlevel, compiled code. A famous example is Java bytecode verification [START_REF] Gosling | Java intermediate bytecodes[END_REF][START_REF] Lindholm | The Java Virtual Machine Specification[END_REF][START_REF] Leroy | Java bytecode verification: an overview[END_REF], which performs static type-checking on JVM bytecode at dynamic loading time. Typed Assembly Language [START_REF] Morrisett | From System F to typed assembly language[END_REF][START_REF] Morrisett | Stack-based typed assembly language[END_REF] goes several steps below virtual machine code: it statically type-checks assembly code for an actual microprocessor (the Intel x86 family), including many advanced idioms such as stack unwinding for exception handling.

Java bytecode verification and typed assembly language leave certain checks relevant to type safety to be performed at run-time: typically, array bound checks, or Java's downcasts. More advanced type systems based on dependent types were proposed to allow static verification of array bound checks (and more) [START_REF] Xi | Eliminating array bound checking through dependent types[END_REF][START_REF] Xi | A dependently typed assembly language[END_REF][START_REF] Shao | A type system for certified binaries[END_REF][START_REF] Crary | An expressive, scalable type theory for certified code[END_REF]. Proof-carrying code [START_REF] Necula | Proof-carrying code[END_REF] takes this approach to the extreme by replacing static type checking with static proof checking in a general program logic: the provider of the code provides not only compiled code, but also a proof that it satisfies a certain security property; the user of the code, then, checks this proof to make sure that the code meets the property. The property typically includes type correctness and memory safety, but can also capture finer behavioral aspects of the code [START_REF] Necula | Safe, untrusted agents using proof-carrying code[END_REF].

Implementing access control

The security policy implemented by access control checks is traditionally represented as an access control matrix, giving for each resource and each principal the allowed operations. This matrix is often represented as access control lists (each resource carries information on which principals can access it) or as capabilities (each principal carries a set of resources that it can access). The yes/no nature of access control matrices is sometimes too coarse: security automata [START_REF] Schneider | Enforceable security policies[END_REF] can be used instead to base access control decisions on the history of the program execution, e.g. to allow an applet to read local files or make network connections, but not both (to prevent information leaks).

Determining the principal that is about to perform a sensitive operation is often difficult. In particular, shared library code that performs operations on behalf of an untrusted user must have lower privileges than when performing operations on behalf of a trusted user. The Java security manager [START_REF] Gong | Inside Java 2 platform security: architecture, API design, and implementation[END_REF] uses stack inspection to address this problem: each method is associated with a principal, and the permissions granted are those of the least privileged principal appearing in the method call stack leading to the current operation. This model is sometimes too restrictive: an applet is typically allowed to draw text on the screen, but not to read files; yet, to draw text on behalf of the applet, the system may need to read fonts from files. Privilege amplification mechanisms are provided to address this need, whereas system code can assert a permission (e.g. read a file for the font loading code) regardless of whether its caller has it.

Access control checks are traditionally performed dynamically, during execution. The run-time overhead of these checks is generally tolerable, and can be further reduced by partial evaluation techniques allowing for instance inline expansion and specialization of security automata [START_REF] Erlingsson | IRM enforcement of Java stack inspection[END_REF][START_REF] Colcombet | Enforcing trace properties by program transformation[END_REF][START_REF] Thiemann | Enforcing security properties by type specialization[END_REF].

Still, it is desirable to perform static approximations of access control checks: to guide and validate optimizations such as removal of redundant checks, but also to help programmers determine whether their code works correctly under a given security policy. Jensen et al. [START_REF] Besson | Secure calling contexts for stack inspection[END_REF] develop a static approximation of the Java stack inspection mechanism, where the (infinitely many) call stacks are abstracted as a finite automaton, and security properties described as temporal formulae are model-checked against this automaton. Pottier et al. [START_REF] Pottier | A systematic approach to static access control[END_REF] compose the security-passing interpretation of stack inspection (proposed in [START_REF] Wallach | The security architecture formerly known as stack inspection: A security mechanism for language-based systems[END_REF] as a dynamic implementation technique) with conventional type systems described in the HM (X) framework to obtain type-based static security analyses. Finally, Walker [START_REF] Walker | A type system for expressive security policies[END_REF] describes a type system for typed assembly language where the states of security automata are expressed within the types themselves, allowing fine static control of the program security behavior.

3 Application to smart card programming

Smart card architectures

Smart cards are small, inexpensive embedded computers used as security tokens in several areas, such as credit cards and mobile phones. Traditional smart cards such as Eurocard-Mastercard-Visa credit cards behave very much like a small file system, with access control on directories and files, and determination of principals via PIN codes.

The newer Java Card architecture [START_REF] Chen | Java Card Technology for Smart Cards: Architecture and Programmer's Guide[END_REF] offers a model closer to an appletenabled Web browser, with several applications running in the same memory space, and post-issuance downloading of new applications. The applications are executed by a virtual machine that is a subset of the JVM. The security of this architecture relies heavily on the type safety of this JVM variant. For access control, the Java security manager based on stack inspection is replaced by a simpler "firewall" that associates owners to Java objects and prevents an application from accessing directly an object owned by another application. Interapplication communications are restricted to invocation of interface methods on objects explicitly declared as "shared".

Formal methods are being systematically applied to many aspects of the Java Card architecture [START_REF] Hartel | Formalizing the safety of Java, the Java virtual machine and Java Card[END_REF]: formal specifications of the virtual machine, applet loading, the firewall, the APIs, and specific applications; and machine proofs of safety properties such as type safety and non-interference. As for program analyses, several approaches to on-card bytecode verification have been proposed [START_REF] Leroy | Bytecode verification for Java smart card[END_REF][START_REF] Deville | Building an "impossible" verifier on a Java Card[END_REF]. Static analyses of firewall access control are described in [START_REF] Caromel | Context inference for static analysis of java card object sharing[END_REF]. Chugunov et al. [START_REF] Chugunov | Model checking multiapplet Java Card applications[END_REF] describe a more general framework for verifying safety properties of Java Card applets by model checking.

Hardware attacks

The software-based security techniques presented in section 2 all assume that the programs execute on reliable, secured hardware: the best software access control will not prevent information leaks if the attacker can simply steal the hard disk containing the confidential data. In practice, hardware security is often ensured by putting the computers in secured premises (locked doors, armed guards).

For smart cards and similar embedded devices, this is not possible: the hardware is physically in the hands of the potential attackers. By construction, a smart card cannot be pulled apart as easily as a PC: smart card hardware is designed to be tamper proof to some extent. Yet, the small size and cost of a smart card does not allow extensive tamper proofing of the kind used for hardware security modules [START_REF] Smith | Building a high-performance, programmable secure coprocessor[END_REF]. Thus, a determined attacker equipped with a good microelectronics laboratory can mount a variety of physical attacks on a smart card [START_REF] Kuhn | Tamper resistance -a cautionary note[END_REF]:

-Non-intrusive observation: perform precise timings of operations; measure power consumption or electromagnetic emissions as a function of time. -Intrusive observation: expose the chip and implant micro-electrodes on some data paths. -Temporary perturbation: introduce "glitches" in the power supply or the external clock signal; "flash" the chip with high-energy particles. -Permanent modification: destroy connections and transistors within the chip.

These attacks can defeat the security of the software in several ways. Power analysis can reveal the sequencing of instructions performed, thus reveal secret data such as the private keys in naive implementation of public-key cryptography [START_REF] Paul | Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems[END_REF]. Perturbations or modifications can prevent some instructions of the program from executing normally: for instance, a taken conditional branch can be skipped, thus deactivating a security check. Variables and registers can also be set to incorrect values, causing for instance a loop intended to send a communication buffer on the serial port to send a complete memory dump instead.

Software countermeasures

The obvious countermeasure to these attacks is to harden the smart card hardware [START_REF] Kuhn | Design principles for tamper-resistant smartcard processors[END_REF]. It is a little known fact that the programs running on smart cards can also be written in ways that complicate hardware attacks. This is surprising, because in general it is nearly impossible for a program to protect itself from execution on malicious hardware. (Some cryptographic techniques such as those described in [START_REF] Loureiro | Extending tamper-proof hardware security to untrusted execution environments[END_REF] address this issue in the context of boolean circuits, but have not been demonstrated to be practical.)

The key to making smart card software more resistant is to notice that hardware attacks cannot change the behavior of the hardware arbitrarily. Permanent modifications are precise but irreversible, thus can be detected from within the program by running frequent self tests, and storing data in a redundant fashion (checksums). Temporary perturbations, on the other hand, are reversible but imprecise: they may cause all the memory to read as all zeroes or all ones for a few milliseconds, but cannot set a particular memory location to a particular value. Thus, their impact can be minimized by data redundancy, and also by control redundancy. For instance, a critical loop can be double-counted, with one counter that increases and another that decreases to zero; execution is aborted if the sum of the two counters is not the expected constant.

Finally, hardware attacks can be made much harder by program randomization. Randomizing data (as in the "blinding" technique for RSA [START_REF] Paul | Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems[END_REF]) renders information gained by power analysis meaningless. Randomizing control (e.g. calling independent subroutines in a random order, or choosing randomly between different implementations of the same function) makes it difficult to perform a perturbation at a given point in the program execution.

Software hardening techniques such as the ones outlined above are currently applied by hand on the source code, and often require assembly programming to get sufficient control on the execution. It is interesting to speculate how modern programming techniques could be used to alleviate this burden. The hardening code could possibly be separated from the main, algorithmic code using aspectoriented programming [START_REF] Kiczales | Aspect-oriented programming[END_REF]. Perhaps some of the hardening techniques are systematic enough to be performed transparently by a compiler, or by a virtual machine interpreter in the case of Java Card. Finally, reasoning about software hardening techniques could require a probabilistic semantics that reflects some of the time-precision characteristics of likely hardware attacks.

Strong typing is also effective at preventing other kinds of attacks such as buffer overflows that cause attacker-provided data to be executed as privileged code.