TACL Seminar Spring '03
Spring '03 Schedule
|Feb 24||Amal Ahmed||Reasoning about Hierarchical Storage||Abstract / Paper|
|Mar 24||Koji Hasebe (Keito)||A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic||Abstract|
|Apr 7||Jay Ligatti||Run-time Policy Enforcement with Security Automata||Abstract|
|Apr 21||Matthew Bridges||Automatic Discovery of Machine Resources||Abstract|
|Apr 25||New Jersey Programming Languages and Systems Seminar (NJPLS)|
|May 12||David Naumann (Stevens)||Using Access Control for Secure Information Flow in a Java-like Language||Abstract / Paper|
|May 13||Adriana Compagnoni (Stevens)||Dependent Session Types for Safety in Concurrent Communications||Abstract|
Reasoning about Hierarchical Storage
In this paper, we develop a new substructural logic that can encode invariants necessary for reasoning about hierarchical storage. We show how the logic can be used to describe the layout of bits in a memory word, the layout of memory words in a region, the layout of regions in an address space, or even the layout of address spaces in a multiprocessing environment. We provide a semantics for our formulas and then apply the semantics and logic to the task of developing a type system for Mini-KAM, a simplified version of the abstract machine used in the ML Kit with regions.
This is joint work with Limin Jia and David Walker.
A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic
A process following a security protocol is represented by a formal proof (of a fragment of linear logic based on the multiset rewriting model), modifying the idea by Cervesato-Durgin-Lincoln-Mitchell-Scedrov, while the (modified) BAN logic (which was first introduced by Burrows-Abadi-Needham) is used as an evaluation semantics on security-properties for processes.
By this method, we can get rid of the so called 'idealization' step in the verification procedure of the BAN framework. In particular, we classify BAN-style belief-inferences into two categories; the inferences which only require some syntactic structure of a process observed by a participant on one hand, and the inferences which require a participant's knowledge on the structure of a protocol and a certain honesty assumption. We call the latter the honesty inferences. We shall show how such honesty inferences are used in the evaluation semantics for the security verification. We also point out that the evaluation inferences on freshness of nonces/keys/messages are classified as in the first category but that some of such inferences lack the information how to evaluate due to the lack of a certain concrete time-constraint setting.
We introduce a natural time-constraint setting in our process/protocol descriptions and enrich the expressive power of the freshness evaluation.
Run-time Policy Enforcement with Security Automata
I will present an analysis of the security policies that can be enforced by monitoring and modifying programs at run time. The monitors, called security automata, are abstract machines that examine the sequence of security-relevant program actions and transform the sequence when it deviates from a specified policy. I will introduce the edit automaton as a powerful and useful instance of a security automaton; its rich set of transformational powers includes the ability to terminate the application, to suppress undesired or dangerous actions without necessarily terminating the application, and to execute additional actions on behalf of the application. After providing a framework for reasoning about security automata in general, I will develop a taxonomy of the security policies enforceable by edit automata and other specific security automata.
This is joint work with Lujo Bauer and David Walker.
Automatic Discovery of Machine Resources
Compilers require detailed knowledge of the underlying architecture to efficiently and effectively perform instruction scheduling. An efficient scheduler maximally utilizes resources while preventing resource oversubscription. Many machine description languages have been proposed and developed to represent resource consumption by instructions in the ISA. This allows compiler writers to automatically retarget the compiler via different descriptions.
However, manually creating a machine description is both a time consuming and error-prone process. This also assumes that all the information necessary to create a machine description is available. High level specification languages help, but still suffer the from the same problems, although to a lesser degree.
Automatically discovering resource usage prevents errors in the machine description by eliminating encoding and maintenance problems. We present techniques for automatically discovering resources used by an ISA as well as methods to improve the efficiency of the search process.
Using Access Control for Secure Information Flow in a Java-like Language
joint work with Anindya Banerjee
Access control mechanisms are widely used with the intent of enforcing confidentiality and other policies, but few formal connections have been made between information flow and access control. Java and C$\sharp$ are object-oriented languages that provide fine-grained access control. An access control list specifies local policy by authorizing permissions for principals (code sources) associated with class declarations; a mechanism called stack inspection checks permissions at run time. An example is given to show how this mechanism can be used to achieve confidentiality goals in situations where a single system call serves callers of differing confidentiality levels and dynamic access control prevents release of high information to low callers. A novel static analysis is given which applies to such examples. %It also handles the information flow introduced by access control. The analysis is shown to ensure a noninterference property formalizing confidentiality.
Dependent Session Types for Safety in Concurrent Communications
We define a type system for concurrent communication combining session types and correspondence assertions. The dependent session types calculus that we obtain is more expressive than the union of its subsystems. While session types allow us to describe the input/output synchronization between processes, and correspondence assertions allow us to ensure that certain code has been executed before other code, enforcing a communication protocol, dependent session types allow us not only to ensure that two processes communicated, but to guarantee the integrity of the information being exchanged. The resulting type system augments session types with effects and thus yields types which may depend on messages read/written prior within the same session. We prove that evaluation preserves typability and that well-typed processes are safe.
This is joint work with Eduardo Bonelli (Stevens) and Elsa Gunter (NJIT).