2,199 papers · page 72 of 110
Many interactive Web services use the CGI interface for communication with clients. They will dynamically create HTML documents that are presented to the client who then resumes the interaction by submitting data through incorporated form fields. This protocol is difficult to sta…
Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because they provide a very general form of definitions for type variables, allow fine-grained co…
Inclusion-based program analyses are implemented by adding new edges to directed graphs. In most analyses, there are many different ways to add a transitive edge between two nodes, namely through each different path connecting the nodes. This path redundancy limits the scalabilit…
Systems that authenticate a user based on a shared secret (such as a password or PIN) normally allow anyone to query whether the secret is a given value. For example, an ATM machine allows one to ask whether a string is the secret PIN of a (lost or stolen) ATM card. Yet such quer…
Certified code is a general mechanism for enforcing security properties. In this paradigm, untrusted mobile code carries annotations that allow a host to verify its trustworthiness. Before running the agent, the host checks the annotations and proves that they imply the host's se…
Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings that can be captured within a single calculus, the Dependency Core Calculus (DCC)…
Java has demonstrated the utility of type systems for mobile code, and in particular their use and implications for security. Security properties rest on the fact that a well-typed Java program (or the corresponding verified bytecode) cannot cause certain kinds of damage.In this …
Relevant context inference (RCI) is a modular technique for flow- and context-sensitive data-flow analysis of statically typed object-oriented programming languages such as C++ and Java. RCI can be used to analyze complete programs as well as incomplete programs such as libraries…
Watermarking embeds a secret message into a cover message. In media watermarking the secret is usually a copyright notice and the cover a digital image. Watermarking an object discourages intellectual property theft, or when such theft has occurred, allows us to prove ownership.T…
Abstract An increasing number of systems rely on programming language technology to ensure safety and security of low-level code. Unfortunately, these systems typically rely on a complex, trusted garbage collector. Region-based type systems provide an alternative to garbage colle…
AnnoDomini is a source-to-source conversion tool for making COBOL programs Year 2000 compliant. It is technically and conceptually built upon type-theoretic techniques and methods: type-based specification, program analysis by type inference and type-directed transformation. Thes…
We extend the tree parsing approach to code selection to DAGs. In general, our extension does not produce the optimal code selection for all DAGs (this problem would be NPcomplete) , but for certain code selection grammars, it does. We present a method for checking whether a code…
There has already been considerable research on constructing modular, monad-based specifications of computational effects (state, exceptions, nondeterminism, etc.) in programming languages. We present a simple framework in this tradition, based on a Church-style effect-typing sys…
Linking is a low-level task that is usually vaguely specified, if at all, by language definitions. However, the security of web browsers and other extensible systems depends crucially upon a set of checks that must be performed at link time. Building upon the simple, but elegant …
) Vineet Gupta Radha Jagadeesan Prakash Panangaden y vgupta@mail.arc.nasa.gov radha@cs.luc.edu prakash@cs.mcgill.ca Caelum Research Corporation Dept. of Math. and Computer Sciences School of Computer Science NASA Ames Research Center Loyola University--Lake Shore Campus McGill Un…
Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which…
Linear types (types of values that can be used just once) have been drawing a great deal of attention because they are useful for memory management, in-place update of data structures, etc.: an obvious advantage is that a value of a linear type can be immediately deallocated afte…
The standard implementation technique for lazy functional languages is call-by-need, which ensures that an argument to a function in any given call is evaluated at most once. A significant problem with call-by-need is that it is difficult -- even for compiler writers -- to predic…
A promising technique for protecting privacy and integrity of sensitive data is to statically check information flow within programs that manipulate the data. While previous work has proposed programming language extensions to allow this static checking, the resulting languages a…
A type system with proven soundness is a prerequisite for the safe and efficient execution of Java bytecode programs. So far, efforts to construct such a type system have followed a forward dataflow approach, in the spirit of the original Java Virtual Machine bytecode verifier. W…