NSumner's Top Recommendations

Abstract

Although distributed threads on distributed shared memory (DSM) provide an easy programming model for distributed computer systems, it is not easy to build a high performance system with them, because a software DSM system is prone to page-thrashing. One way to reduce page-thrashing is to utilize thread migration, which leads to changes in page access patterns on DSM.In this paper, we propose thread scheduling methods based upon page access information and discuss an analytical model for evaluating this information. Then, we ...

Abstract

Dynamic detection of likely invariants is a program analysis that generalizes over observed values to hypothesize program properties. The reported program properties are a set of likely invariants over the program, also known as an operational abstraction. Operational abstractions are useful in testing, verification, bug detection, refactoring, comparing behavior, and many other tasks. ...

Abstract

Programs written in languages that provide direct access tomemory through pointers often contain memory-related faults, which may cause non-deterministic failures and even security vulnerabilities. In this paper, we present a new technique based on dynamic tainting for protecting programs from illegal memory accesses. When memory is allocated, at runtime, our technique taints both the memory and the corresponding pointer using the same taint mark. Taint marks are then suitably propagated while the program executes and are checked every time a memory ...

Abstract

Explicitly stated program invariants can help programmers by characterizing certain aspects of program execution and identifying program properties that must be preserved when modifying code. Unfortunately, these invariants are usually absent from code. Previous work showed how to dynamically detect invariants from program traces by looking for patterns in and relationships among variable values. A prototype implementation, Daikon, accurately recovered invariants from formally-specified programs, and the invariants it detected in other programs assisted programmers in a software evolution task. However, Daikon ...

Abstract

Dynamic binary instrumentation (DBI) frameworks make it easy to build dynamic binary analysis (DBA) tools such as checkers and profilers. Much of the focus on DBI frameworks has been on performance; little attention has been paid to their capabilities. As a result, we believe the potential of DBI has not been fully exploited. ...

Abstract

Several existing dynamic binary analysis tools use shadowmemory -they shadow, in software, every byte of memory used by a program with another value that says something about it. Shadow memory is difficult to implement both efficiently and robustly. Nonetheless, existing shadow memory implementations have not been studied in detail. This is unfortunate, because shadow memory is powerful-for example, some of the existing tools that use it detect critical errors such as bad memory accesses, data races, and uses of uninitialised ...

Abstract

This paper introduces DIDUCE, a practical and effective tool that aids programmers in detecting complex program errors and identifying their root causes. By instrumenting a program and observing its behavior as it runs, DIDUCE dynamically formulates hypotheses of invariants obeyed by the program. DIDUCE hypothesizes the strictest invariants at the beginning, and gradually relaxes the hypothesis as violations are detected to allow for new behavior. The violations reported help users to catch software bugs as soon as they occur. They also ...

Abstract

This paper presents the initial results of a project to determine if the techniques of proof-carrying code and certifying compilers can be applied to programming languages of realistic size and complexity. The experiment shows that: (1) it is possible to implement a certifying native-code compiler for a large subset of the Java programming language; (2) the compiler is freely able to apply many standard local and global optimizations; and (3) the PCC binaries it produces are of reasonable size... ...

Abstract

Concurrent programming is notoriously di#cult. Current abstractions are intricate and make it hard to design computer systems that are reliable and scalable. We argue that these problems can be addressed by moving to a declarative style of concurrency control in which programmers directly indicate the safety properties that they require. ...

Abstract

We describe a framework for adding type qualifiers to a language. Type qualifiers encode a simple but highly useful form of subtyping. Our framework extends standard type rules to model the flow of qualifiers through a program, where each qualifier or set of qualifiers comes with additional rules that capture its semantics. Our framework allows types to be polymorphic in the type qualifiers. We present a const-inference system for C as an example application of the framework. We show that for ...

Abstract

The future annotations of MultiLisp provide a simple method for taming the implicit parallelism of functional programs. Past research concerning futures has focused on implementation issues. In this paper, we present a series of operational semantics for an idealized functional language with futures with varying degrees of intensionality. We develop a set-based analysis algorithm from the most intensional semantics, and use that algorithm to perform touch optimization on programs. Experiments... ...

Abstract

Distinguishing non-null references from possibly-null references at the type level can detect null-related errors in objectoriented programs at compile-time. This paper gives a proposal for retrofitting a language such as C# or Java with non-null types. It addresses the central complications that arise in constructors, where declared non-null fields may not yet have been initialized, but the partially constructed object is already accessible. The paper reports experience with an implementation ... ...

Abstract

this paper appears in the proceedings of ECOOP 2002 ObjectOriented Programming, LNCS 2374, June 2002. The prototype implementation described in the paper will shortly be available from ...

Abstract

Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions, between threads. Previous work addressed this problem by devising tools for detecting race conditions , a situation where two threads simultaneously access the same data variable, and at least one of the accesses is a write. Unfortunately, verifying the absence of such simultaneous-access race conditions is neither necessary nor sufficient to ensure the absence of errors due to unexpected thread interactions.We propose that ...

Abstract

We present a novel approach to dynamic datarace detection for multithreaded object-oriented programs. Past techniques for onthe -fly datarace detection either sacrificed precision for performance, leading to many false positive datarace reports, or maintained precision but incurred significant overheads in the range of 3# to 30#. In contrast, our approach results in very few false positives and runtime overhead in the 13% to 42% range, making it both efficient and precise. This performance... ...

Abstract

This paper presents a static race detection analysis for multithreaded Java programs. Our analysis is based on a formal type system that is capable of capturing many common synchronization patterns. These patterns include classes with internal synchronization, classes that require client-side synchronization, and thread-local classes. Experience checking over 40,000 lines of Java code with the type system demonstrates that it is an effective approach for eliminating races conditions. On large... ...

Abstract

Allowing method invocations in program specifications increases modularity and comprehensibility and is as important in specifications as it is in the program itself. However, method invocations do not map neatly into the first-order logics that are often used for assuring the correctness of specifications. One problem is translating specifications in a way that acknowledges the potential for exceptional behavior. The ESC/Java2 tool has been able to achieve a practical translation of method... ...

Abstract

Modules and objects both contain variables whose values may be constrained by invariants. For example, in the object-oriented languages Java and C#, a module is a class and its static fields, and an object is an instance of a class and its instance variables. The invariants of modules work differently both from the invariants of objects alone and from the invariants of modules in a procedural language. This paper presents a methodology for module invariants in an objectoriented setting. The... ...

Abstract

This paper distinguishes several different approaches to organising a Weakest Precondition (WP) calculus in a theorem prover. The implementation of two of these approaches for Java within the LOOP project is described. This involves the WP-infrastructures in the higher order logic of the theorem prover PVS, together with some associated rules and strategies for automatically proving JML specifications for Java implementations. The soundness of all WP-rules has been proven on the basis of the... ...

Abstract

society today. This thesis presents a new type system that addresses this problem by statically preventing several important classes of programming errors. If a program type checks, we guarantee at compile time that the program does not contain any of those errors. We designed our type system in the context of a Java-like object-oriented language; we call the resulting system SafeJava. The SafeJava type system oers signi cant software engineering bene ts. Speci cally, it provides a... ...

Abstract

The possibility of aliasing between objects constitutes one of the primary challenges in understanding and reasoning about correctness of object-oriented programs. Ownership types provide a principled way of specifying statically enforcable restrictions on object aliasing. Ownership types have been used to aid program understanding and evolution, verify absence of data races and deadlocks in multithreaded programs, and verify absence of memory errors in programs with explicit deallocation. ...

Abstract

This paper presents a new static type system for multi-threaded programs; well-typed programs in our system are guaranteed to be free of data races and deadlocks. Our type system allows programmers to partition the locks into a fixed number of equivalence classes and specify a partial order among the equivalence classes. The type checker then statically verifies that whenever a thread holds more than one lock, the thread acquires the locks in the descending order. Our system also allows... ...

Abstract

This paper describes a type system that is capable of expressing and enforcing immutability constraints. The specific constraint expressed is that the abstract state of the object to which an immutable reference refers cannot be modified using that reference. The abstract state is (part of) the transitively reachable state: that is, the state of the object and all state reachable from it by following references. The type system permits explicitly excluding fields or objects from the abstract... ...

Abstract

Object Model [Sny91], we assume that all method argument and result passing is performed in a manner classically described as "by-reference", but perhaps better labelled as "by-identity". Objects may be accessed "directly" through a bound variable or pseudovariable, or "indirectly" through the instance variables of other objects. More generally an access path is a sequence of variable names. The evaluation of the first variable within the current context yields a new context that is an object... ...

Abstract

Object-oriented programming languages allow inter-object aliasing. Although necessary to construct linked data structures and networks of interacting objects, aliasing is problematic in that an aggregate object's state can change via an alias to one of its components, without the aggregate being aware of any aliasing. Ownership types form a static type system that indicates object ownership. This provides a flexible mechanism to limit the visibility of object references and restrict access... ...

Abstract

A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program. Modular checking requires that each module be accompanied by annotations that specify the module. To help reduce the cost of writing specifications, this paper presents Houdini, an annotation assistant for the modular checker ESC/Java. To infer suitable ESC/Java annotations for a given program, Houdini generates a large number of candidate... ...

Abstract

Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Typically, such policies are described as high-level security properties, stating for example that no pin verification must take place within a transaction. ...

Abstract

Memory consumption policies provide a means to control resource usage on constrained devices, and play an important role in ensuring the overall quality of software systems, and in particular resistance against resource exhaustion attacks. Such memory consumption policies have been previously enforced through static analysis, which yield automatic bounds at the cost of precision, or run-time analysis, which incur an overhead that is not acceptable for constrained devices. In this paper, we study the use of logical methods to specify and ...

Abstract

This paper presents experiments on formal validation of Java applets. It describes a tool that has been developed at the Gemplus Research Labs. This tool allows to formally prove Java classes annotated with JML, an annotation language for Java that provides a framework for specifying class invariants and methods behaviours. The foundations and the main features of the tool are presented. The most innovative part of the tool is that it is tailored to be used by Java programmers, without... ...

Abstract

. Proof-Carrying Code (PCC) enables a computer system to determine, automatically and with certainty, that program code provided by another system is safe to install and execute without requiring interpretation or run-time checking. PCC has applications in any computing system in which the safe, efficient, and dynamic installation of code is needed. The key idea of Proof-Carrying is to attach to the code an easily-checkable proof that its execution does not violate the safety policy of the... ...

Abstract

This paper presents a logical framework derived from the Edinburgh Logical Framework (LF) [5] that can be used to obtain compact representations of proofs and efficient proof checkers. These are essential ingredients of any application that manipulates proofs as first-class objects, such as a Proof-Carrying Code [11] system, in which proofs are used to allow the easy validation of properties of safety-critical or untrusted code. Our framework, which we call LF i , inherits from LF the... ...

Abstract

This paper presents the design and implementation of a compiler that translates programs written in a type-safe subset of the C programming language into highly optimized DEC Alpha assembly language programs, and a certifier that automatically checks the type safety and memory safety of any assembly language program produced by the compiler. The result of the certifier is either a formal proof of type safety or a counterexample pointing to a potential violation of the type system by the... ...

Abstract

This paper describes a mechanism by which an operating system kernel can determine with certainty that it is safe to execute a binary supplied by an untrusted source. The kernel first defines a safety policy and makes it public. Then, using this policy, an application can provide binaries in a special form called proof-carrying code, or simply PCC. Each PCC binary contains, in addition to the native code, a formal proof that the code obeys the safety policy. The kernel can ...

Abstract

Introduction The advent of the World-Wide Web and the rising popularity of the Java programming language have made the problem of mobile-code security one of the focal points of research in Computer Science today. By allowing code to be installed dynamically and then executed, a host system can provide an flexible means of access to its internal resources. Of course, the idea of installing and executing new software on a system is not new. What is new, however, is the potential for a large... ...

Abstract

Introduction A powerful method of interaction between two software systems is through mobile code. By allowing code to be installed dynamically and then executed, a host system can provide a flexible means of access to its internal resources and services. There are many problems to be solved before such uses of untrusted code can become practical. For this position paper, we will focus on the problem of how to establish guarantees about the intrinsic behavior of untrusted programs. Of... ...

Abstract

Explicitly stated program invariants can help programmers by characterizing aspects of program execution and identifying program properties that must be preserved when modifying code. Unfortunately, these invariants are usually absent from code. Previous work showed how to dynamically infer invariants from program traces by looking for patterns in and relationships among variable values. Although the original prototype recovered invariants from formally-specified programs, and the invariants it ... ...

Abstract

Explicitly stated program invariants can help programmers by identifying program properties that must be preserved when modifying code. In practice, however, these invariants are usually implicit. An alternative to expecting programmers to fully annotate code with invariants is to automatically infer invariants from the program itself. This research focuses on dynamic techniques for discovering invariants from execution traces. This paper reports two results. First, it describes techniques for... ...

Abstract

This research proposes and evaluates techniques for selecting predicates for conditional program properties | that is, implications such as p ) q whose consequent is true only when the predicate is true. Conditional properties are prevalent in recursive data structures, which behave dierently in their base and recursive cases, and in many other situations. The experimental context of the research is dynamic detection of likely program invariants, but the ideas should also be applicable to... ...

Abstract

Dynamic detection of likely invariants is a program analysis that generalizes over observed values to hypothesize program properties. The reported program properties are a set of likely invariants over the program, also known as an operational abstraction. Operational abstractions are useful in testing, verification, bug detection, refactoring, comparing behavior, and many other tasks. Previous techniques for... ...

Abstract

data types, modules, packages; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- Pre- and post-conditions; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- Specification techniques. Submitted for publication. c fl Krishna Kishore Dhara and Gary T. Leavens, 1995. Copies may be made for research and scholarly purposes, but not for direct commercial advantage. All rights reserved. Department of... ...

Abstract

This paper defines a programming methodology for using object invariants. The methodology, which enriches a program's state space to express when each object invariant holds, deals with owned object components, ownership transfer, and subclassing, and is expressive enough to allow many interesting object-oriented programs to be specified and verified. Lending itself to sound modular verification, the methodology also provides a solution to the problem of determining what state a method is... ...

Abstract

Writing concurrent programs is notoriously difficult, and is of increasing practical importance. A particular source of concern is that even correctly-implemented concurrency abstractions cannot be composed together to form larger abstractions. In this paper we present a new concurrency model, based on transactional memory , that offers far richer composition. All the usual benefits of transactional memory are present (e.g. freedom from deadlock), but in addition we describe new modular forms of blocking and choice that ...

Abstract

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed -calculus with dependent types. Syntax is treated in a style similar to, but more general than, Martin-Löf's system of arities. The treatment of rules and proofs focuses on his notion of a judgement. Logics are represented in LF via a new principle, the judgements as types principle, whereby each judgement is ...

Abstract

The specification language JML (Java Modelling Language) includes so-called assignable clauses, also known as modifies clauses, for specifying which fields may change their value as side-effect of a method. This paper uses abstract interpretation over a trace semantics for a simple object-oriented language to define a correct static analysis for checking the correctness of assignable clauses. ...

Abstract

We present a modular specification technique for frame properties. The technique uses modifies clauses and abstract fields with declared dependencies. Modularity is guaranteed by a programming model that restricts aliasing, and by modularity requirements for dependencies. For concreteness, we adapt this technique to the Java Modeling Language, JML. ...

Abstract

We present a new method purity analysis for Java programs. A method is pure if it does not mutate any location that exists in the program state right before method invocation. Our analysis is built on top of a combined pointer and escape analysis for Java programs and is capable of determining that methods are pure even when the methods do heap mutation, provided that the mutation affects only objects created after the beginning of the method. Because our analysis extracts... ...

Abstract

Java is typically compiled into an intermediate language, JVML, that is interpreted by the Java Virtual Machine. Because mobile JVML code is not always trusted, a bytecode verifier enforces static constraints that prevent various dynamic errors. Given the importance of the bytecode verifier for security, its current descriptions are inadequate. This paper proposes using typing rules to describe the bytecode verifier because they are more precise than prose, clearer than code, and easier to... ...

Abstract

Java Bytecode Verification ensures that bytecode can be trusted to avoid various dynamic runtime errors, but it requires an analysis which is currently unrealistic to implement on systems with very sparse resources such as Sun's Java Cards featuring a reduced Java virtual machine embedded on a smartcard (credit card with an integrated microprocessor). Commonly it is assumed that verification has to be performed off-card and shipped by means of cryptographic protection techniques, e.g.,... ...

Abstract

. Java bytecode verification forms the basis for Java-based Internet security and needs a rigorous description. One important aspect of bytecode verification is to check if a Java Virtual Machine (JVM) program is statically well-typed. So far several formal specifications have been proposed to define what the static welltypedness means. This paper takes a step further and presents a chaotic fixpoint iteration, which represents a family of fixpoint computation strategies to compute a least type... ...

Abstract

. In this chapter we formally specify a subset of Java Virtual Machine (JVM) instructions for objects, methods and subroutines based on the official JVM Specification, the official Java Language Specification and Sun's JDK 1.1.4 implementation of the JVM. Our formal specification describes the runtime behaviors of the instructions in relevant memory areas as state transitions and most structural and linking constraints on the instructions as a static typing system. The typing system includes a... ...

Abstract

We provide an abstract interpretation for Java bytecode programs to build finite state models of these programs. We describe the bytecode constraints as CTL formulas which can be checked against the finite models by a (standard) model checker. We see a practical way to perform bytecode verification on a formal basis in that it could help to achieve higher security and open the door for further extensions to prove additional properties of Java bytecode. ...

Abstract

This paper presents a novel approach to the problem of bytecode verification for Java Card applets. Owing to its low memory requirements, our verification algorithm is the first that can be embedded on a smart card, thus increasing tremendously the security of post-issuance downloading of applets on Java Cards. ...

Abstract

The SLam calculus is a typed -calculus that maintains security information as well as type information. The type system propagates security information for each object in four forms: the object's creators and readers, and the object's indirect creators and readers (i.e., those agents who, through flowof -control or the actions of other agents, can influence or be influenced by the content of the object). We prove that the type system prevents security violations and give some examples of its... ...

Abstract

In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another site, where it is then interpreted by the Java Virtual Machine. Since bytecode may be written by hand, or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier that performs a number of consistency checks before code is interpreted. As illustrated by previous attacks on the Java Virtual Machine, these tests,... ...

Abstract

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static Checker for Java (ESC/Java), an experimental compile-time program checker that finds common programming errors. The checker is powered by verification-condition generation and automatic theoremproving techniques. It provides programmers with a simple annotation language with which programmer design... ...

Abstract

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), a small extension of Moggi's computational lambda calculus. To establish this thesis, we translate typed calculi for secure information flow, binding-time analysis, slicing, and call-tracking into DCC. The... ...

Abstract

Specification languages that use the same expression language as the implementation language must decide whether or not to permit functional abstraction, i.e., method calls in specification expressions. The difficulty is that a specification must not change the functional behavior of the associated program. ...