Difference between revisions of "TACL Seminar Fall '02"

From CSWiki
Jump to: navigation, search
m (Amal Ahmed)
m (Fall '02 Schedule)
Line 10: Line 10:
 
| Dec 10 || [http://ece-www.colorado.edu/~manishv/ Manish Vachharajani] || A Component Composition and Customization Language for the Liberty Simulation Environment || [[TACL_Seminar_Fall_'02#Manish_Vachharajani | Abstract]]
 
| Dec 10 || [http://ece-www.colorado.edu/~manishv/ Manish Vachharajani] || A Component Composition and Customization Language for the Liberty Simulation Environment || [[TACL_Seminar_Fall_'02#Manish_Vachharajani | Abstract]]
 
|-
 
|-
| Jan 9 || Amal Ahmed || The Logical Approach to Stack Typing || [[TACL_Seminar_Fall_'02#Amal_Ahmed_1 | Abstract]]
+
| Jan 9 || Amal Ahmed || The Logical Approach to Stack Typing || [[TACL_Seminar_Fall_'02#Amal_Ahmed | Abstract]]
 
|-
 
|-
 
| Jan 10 || Gang Tan || Enforcing Resource Usage Protocols via Scoped Methods || [[TACL_Seminar_Fall_'02#Gang_Tan | Abstract]]
 
| Jan 10 || Gang Tan || Enforcing Resource Usage Protocols via Scoped Methods || [[TACL_Seminar_Fall_'02#Gang_Tan | Abstract]]

Revision as of 03:33, 27 August 2006

TACL Seminar

Fall '02 Schedule

Date Speaker Title Links
Dec 3 Sudhakar Govindavajhala Using Memory Errors to Attack a Virtual Machine Abstract
Dec 10 Manish Vachharajani A Component Composition and Customization Language for the Liberty Simulation Environment Abstract
Jan 9 Amal Ahmed The Logical Approach to Stack Typing Abstract
Jan 10 Gang Tan Enforcing Resource Usage Protocols via Scoped Methods Abstract

Abstracts

Sudhakar Govindavajhala

Using Memory Errors to Attack a Virtual Machine

We present an experimental study showing that soft memory errors can lead to serious security vulnerabilities in Java and .NET virtual machines, or in any system that relies on type-checking of untrusted programs as a protection mechanism. Our attack works by sending to the JVM for execution a Java program that is designed so that almost any memory error in its address space will allow it to take control of the JVM. All conventional Java and .NET virtual machines are vulnerable to this attack. The technique of the attack is broadly applicable against other language-based security schemes such as proof-carrying code.

We measured the attack on two commercial Java Virtual Machines: Sun's and IBM's. We show that a single-bit error in the Java program's data space can be exploited to execute arbitrary code with a probability of about 70%, and multiple-bit errors with a lower probability.

Our attack is particularly relevant against smart cards or tamper-resistant computers, where the user has physical access (to the outside of the computer) and can use various means to induce faults; we have successfully used heat. Fortunately, there are some straightforward defenses against this attack.

This is joint work with Andrew Appel.

Manish Vachharajani

A Component Composition and Customization Language for the Liberty Simulation Environment

During hardware design, system architects use simulation extensively to validate and guide design decisions. To facilitate construction of these simulators we developed the Liberty Simulation Environment (LSE). LSE consists of a library of components, the Liberty Simulator Specification (LSS) language, and a tool that constructs a simulator based on the library and an LSS provided by the user.

In this talk, we will discuss the design considerations and tradeoffs made while developing the Liberty Simulator Specification language. The LSS language is unique in that it is designed not to specify the execution of a simulator, but rather to specify how components should be composed and customized to build a simulator. The LSS language combines several programming language techniques, including type inference and aspects, and non-standard evaluation semantics for object instantiation to ease the construction of simulators.

Amal Ahmed 1

The Logical Approach to Stack Typing

To appear in TLDI 03 (Types in Language Design and Implementation)

We develop a logic for reasoning about adjacency and separation of memory blocks, as well as aliasing of pointers. We provide a memory model for our logic and present a sound set of natural deduction-style inference rules. We deploy the logic in a simple type system for a stack-based assembly language. The connectives for the logic provide a flexible yet concise mechanism for controlling allocation, deallocation and access to both heap-allocated and stack-allocated data.

This is joint work with David Walker.

Gang Tan

Enforcing Resource Usage Protocols via Scoped Methods

To appear in FOOL 10 (Foundations of Object-Oriented Languages)

Traditional modularity mechanisms such as Java's classes and packages or ML's structures and functors restrict the set of functions that may be applied to an object, but are unable to restrict the timing of these function applications effectively. We propose a new language construct, the scoped method, which allows the implementer of a class to specify a temporal resource usage protocol. This protocol limits the sequence of methods that may be applied to an object. For example, a protocol for file access might specify that the file must be opened, read or written some number of times, and then closed. We present a type-based analysis to enforce the protocol and prove its correctness.

This is joint work with Xinming Ou and David Walker.



TACL Seminar