Many proofs of interactive cryptographic protocols (e.g., as in Universal Composability) operate by proving the protocol at hand to be observationally equivalent to an idealized specification. While pervasive, formal tool support for observational equivalence of cryptographic protocols is still a nascent area of research. Current mechanization efforts tend to either focus on diff-equivalence, which establishes observational equivalence between protocols with identical control structures, or require an explicit witness for the observational equivalence in the form of a bisimulation relation. Our goal is to simplify proofs for cryptographic protocols by introducing a core calculus, IPDL, for cryptographic observational equivalences. Via IPDL, we aim to address a number of theoretical issues for cryptographic proofs in a simple manner, including probabilistic behaviors, distributed message-passing, and resource-bounded adversaries and simulators. We demonstrate IPDL on a number of case studies, including a distributed coin toss protocol, Oblivious Transfer, and the GMW multi-party computation protocol. All proofs of case studies are mechanized via an embedding of IPDL into the Coq proof assistant.

File formats specify how data is encoded for persistent storage. They cannot be formalized as context-free grammars since their specifications include context-sensitive patterns such as the random access pattern and the type-length-value pattern. We propose a new grammar mechanism called Interval Parsing Grammars IPGs) for file format specifications. An IPG attaches to every nonterminal/terminal an interval, which specifies the range of input the nonterminal/terminal consumes. By connecting intervals and attributes, the context-sensitive patterns in file formats can be well handled. In this paper, we formalize IPGs' syntax as well as its semantics, and its semantics naturally leads to a parser generator that generates a recursive-descent parser from an IPG. In general, IPGs are declarative, modular, and enable termination checking. We have used IPGs to specify a number of file formats including ZIP, ELF, GIF, PE, and part of PDF; we have also evaluated the performance of the generated parsers.

We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing a compact representation of a bisimulation, using "leaps." Proofs are powered by a certified compilation chain from first-order entailments to low-level bitvector verification conditions, which are discharged using off-the-shelf SMT solvers. As a result, parser equivalence proofs in Leapfrog are fully automatic and push-button.

The problem of probabilistic modeling and inference, at a high-level, can be viewed as constructing a (model, query, inference) tuple, where an inference algorithm implements a query on a model. Notably, the derivation of inference algorithms can be a difficult and error-prone task. Hence, researchers have explored how ideas from probabilistic programming can be applied. In the context of constructing these tuples, probabilistic programming can be seen as taking a language-based approach to probabilistic modeling and inference. For instance, by using (1) appropriate languages for expressing models and queries and (2) devising inference techniques that operate on encodings of models (and queries) as program expressions, the task of inference can be automated.

The Coq proof assistant is increasingly used for constructing verified software, including everything from verified microkernels to verified databases. Programmers typically write code in Gallina (the core functional language of Coq) and construct proofs about those Gallina programs. Then, through a process of "extraction", the Gallina code is translated to either OCaml, Haskell, or Scheme and compiled by a conventional compiler to produce machine code. Unfortunately, this translation often results in inefficient code, and it fails to take advantage of the dependent types and proofs. Furthermore, it's a bit embarrassing that the process is not formally verified.

We present a mechanized proof of security for an efficient Searchable Symmetric Encryption (SSE) scheme completed in the Foundational Cryptography Framework (FCF). FCF is a Coq library for reasoning about cryptographic schemes in the computational model that features a small trusted computing base and an extensible design. Through this effort, we provide the first mechanized proof of security for an efficient SSE scheme, and we demonstrate that FCF is well-suited to reasoning about such complex protocols.

To study the emergence of cooperative behavior, we have developed a scalable parallel framework for evolutionary game dynamics. This is a critical computational tool enabling large-scale agent simulation research. An important aspect is the amount of history, or memory steps, that each agent can keep. When six memory steps are taken into account, the strategy space spans 24096 potential strategies, requiring large populations of agents. We introduce a multi-level decomposition method that allows us to exploit both multi-node and thread-level parallel scaling while minimizing communication overhead. We present the results of a production run modeling up to six memory steps for populations consisting of up to 1018 agents, making this study one of the largest yet undertaken. The high rate of mutation within the population results in a non-trivial parallel implementation. The strong and weak scaling studies provide insight into parallel scalability and programmability trade-offs for large-scale simulations, while exhibiting near perfect weak and strong scaling on 16,384 tasks on Blue Gene/Q. We further show 99% weak scaling up to 294,912 processors 82% strong scaling efficiency up to 262,144 processors of Blue Gene/P. Our framework marks an important step in the study of game dynamics with potential applications in fields ranging from biology to economics and sociology.

Existing designs for fine-grained, dynamic information-flow control assume that it is acceptable to terminate the entire system when an incorrect flow is detected-i.e, they give up availability for the sake of confidentiality and integrity. This is an unrealistic limitation for systems such as long-running servers. We identify public labels and delayed exceptions as crucial ingredients for making information-flow errors recoverable in a sound and usable language, and we propose two new error-handling mechanisms that make all errors recoverable. The first mechanism builds directly on these basic ingredients, using not-a-values (NaVs) and data flow to propagate errors. The second mechanism adapts the standard exception model to satisfy the extra constraints arising from information flow control, converting thrown exceptions to delayed ones at certain points. We prove that both mechanisms enjoy the fundamental soundness property of non-interference. Finally, we describe a prototype implementation of a full-scale language with NaVs and report on our experience building robust software components in this setting.

For performance and for incorporating legacy libraries, many Java applications contain native-code components written in unsafe languages such as C and C++. Native-code components interoperate with Java components through the Java Native Interface (JNI). As native code is not regulated by Java's security model, it poses serious security threats to the managed Java world. We introduce a security framework that extends Java's security model and brings native code under control. Leveraging software-based fault isolation, the framework puts native code in a separate sandbox and allows the interaction between the native world and the Java world only through a carefully designed pathway. Two different implementations were built. In one implementation, the security framework is integrated into a Java Virtual Machine (JVM). In the second implementation, the framework is built outside of the JVM and takes advantage of JVM-independent interfaces. The second implementation provides JVM portability, at the expense of some performance degradation. Evaluation of our framework demonstrates that it incurs modest runtime overhead while significantly enhancing the security of Java applications.

Software-based fault isolation (SFI), as used in Google's Native Client (NaCl), relies upon a conceptually simple machine-code analysis to enforce a security policy. But for complicated architectures such as the x86, it is all too easy to get the details of the analysis wrong. We have built a new checker that is smaller, faster, and has a much reduced trusted computing base when compared to Google's original analysis. The key to our approach is automatically generating the bulk of the analysis from a declarative description which we relate to a formal model of a subset of the x86 instruction set architecture. The x86 model, developed in Coq, is of independent interest and should be usable for a wide range of machine-level verification tasks.

In many software attacks, inducing an illegal control-flow transfer in the target system is one common step. Control-Flow Integrity (CFI) protects a software system by enforcing a pre-determined control-flow graph. In addition to providing strong security, CFI enables static analysis on low-level code. This paper evaluates whether CFI-enabled static analysis can help build efficient and validated data sandboxing. Previous systems generally sandbox memory writes for integrity, but avoid protecting confidentiality due to the high overhead of sandboxing memory reads. To reduce overhead, we have implemented a series of optimizations that remove sandboxing instructions if they are proven unnecessary by static analysis. On top of CFI, our system adds only 2.7% runtime overhead on SPECint2000 for sandboxing memory writes and adds modest 19% for sandboxing both reads and writes. We have also built a principled data-sandboxing verifier based on range analysis. The verifier checks the safety of the results of the optimizer, which removes the need to trust the rewriter and optimizer. Our results show that the combination of CFI and static analysis has the potential of bringing down the cost of general inlined reference monitors, while maintaining strong security.

Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation validators do so by trying to match the value-graphs of an original function and its transformed counterpart. In this paper, we present the design of such a validator for LLVM's intra-procedural optimizations, a design that does not require any instrumentation of the optimizer, nor any rewriting of the source code to compile, and needs to run only once to validate a pipeline of optimizations. We present the results of our preliminary experiments on a set of benchmarks that include GCC, a perl interpreter, SQLite3, and other C programs.

Safe is a clean-slate design for a secure host architecture. It integrates advances in programming languages, operating systems, and hardware and incorporates formal methods at every step. Though the project is still at an early stage, we have assembled a set of basic architectural choices that we believe will yield a high-assurance system. We sketch the current state of the design and discuss several of these choices.

Java applications often need to incorporate native-code components for efficiency and for reusing legacy code. However, it is well known that the use of native code defeats Java's security model. We describe the design and implementation of Robusta, a complete framework that provides safety and security to native code in Java applications. Starting from software-based fault isolation (SFI), Robusta isolates native code into a sandbox where dynamic linking/loading of libraries in supported and unsafe system modification and confidentiality violations are prevented. It also mediates native system calls according to a security policy by connecting to Java's security manager. Our prototype implementation of Robusta is based onNative Client and OpenJDK. Experiments in this prototype demonstrate Robusta is effective and efficient, with modest runtime overhead on a set of JNI benchmark programs. Robusta can be used to sandbox native libraries used in Java's system classes to prevent attackers from exploiting bugs in the libraries. It can also enable trustworthy execution of mobile Java programs with native libraries. The design of Robusta should also be applicable when other type-safe languages (e.g., C#, Python) want to ensure safe interoperation with native libraries

We describe Nikola, a first-order language of array computations embedded in Haskell that compiles to GPUs via CUDA using a new set of type-directed techniques to support re-usable computations. Nikola automatically handles a range of low-level details for Haskell programmers, such as marshaling data to/from the GPU, size inference for buffers, memory management, and automatic loop parallelization. Additionally, Nikola supports both compile-time and run-time code generation, making it possible for programmers to choose when and where to specialize embedded programs.

We report on our experience implementing a lightweight, fully verified relational database management system (RDBMS). The functional specification of RDBMS behavior, RDBMS implementation, and proof that the implementation meets the specification are all written and verified in Coq. Our contributions include: (1) a complete specification of the relational algebra in Coq; (2) an efficient realization of that model (B+ trees) implemented with the Ynot extension to Coq; and (3) a set of simple query optimizations proven to respect both semantics and run-time cost. In addition to describing the design and implementation of these artifacts, we highlight the challenges we encountered formalizing them, including the choice of representation for finite relations of typed tuples and the challenges of reasoning about data structures with complex sharing. Our experience shows that though many challenges remain, building fully-verified systems software in Coq is within reach.

We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules.

We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.

Applications that combine live data streams with embedded, parallel, and distributed processing are becoming more commonplace. WaveScript is a domain-specific language that brings high-level, type-safe, garbage-collected programming to these domains. This is made possible by three primary implementation techniques, each of which leverages characteristics of the streaming domain. First, we employ a novel evaluation strategy that uses a combination of interpretation and reification to partially evaluate programs into stream dataflow graphs. Second, we use profile-driven compilation to enable many optimizations that are normally only available in the synchronous (rather than asynchronous) dataflow domain. Finally, we incorporate an extensible system for rewrite rules to capture algebraic properties in specific domains (such as signal processing).

Abstract We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and nontermination. We propose Hoare type theory (HTT), which incorporates Hoare-style specifications into types, making it possible to statically track and enforce correct use of side effects. The main feature of HTT is the Hoare type { P } x : A { Q } specifying computations with precondition P and postcondition Q that return a result of type A . Hoare types can be nested, combined with other types, and abstracted, leading to a smooth integration with higher-order functions and type polymorphism. We further show that in the presence of type polymorphism, it becomes possible to interpret the Hoare types in the “small footprint” manner, as advocated by separation logic, whereby specifications tightly describe the state required by the computation. We establish that HTT is sound and compositional, in the sense that separate verifications of individual program components suffice to ensure the correctness of the composite program.

The development of high-level programming environments is essential if wireless sensor networks are to be accessible to non-experts. In this paper, we present the Regiment system, which consists of a high-level language for spatiotemporal macroprogramming, along with a compiler that translates global programs into node-level code. In Regiment, the programmer views the network as a set of spatially-distributed data streams. The programmer can manipulate sets of these streams that may be defined by topological or geographic relationships between nodes. Regiment provides a rich set of primitives for processing data on individual streams, manipulating regions, performing aggregation over a region, and triggering new computation within the network.

Java bug finders perform static analysis to find implementation mistakes that can lead to exploits and failures; Java compilers perform static analysis for optimization.allIf Java programs contain foreign function calls to C libraries, however, static analysis is forced to make either optimistic or pessimistic assumptions about the foreign function calls, since models of the C libraries are typically not available.

A great deal of recent work has investigated new programming abstractions and models for sensor networks. However, the complexity of such systems demands a great deal of effort to develop appropriate compilers and runtime platforms to achieve good performance. We will demonstrate Flask [5], a new programming platform for sensor networks that decouples the design of a high-level programming environment from the the low-level details of generating per-node code and an efficient runtime system.

In previous work, we proposed a Hoare Type Theory (HTT) which combines effectful higher-order functions, dependent types and Hoare Logic specifications into a unified framework. However, the framework did not support polymorphism, and ailed to provide a modular treatment of state in specifications. In this paper, we address these shortcomings by showing that the addition of polymorphism alone is sufficient for capturing modular state specifications in the style of Separation Logic. Furthermore, we argue that polymorphism is an essential ingredient of the extension, as the treatment of higher-order functions requires operations not encodable via the spatial connectives of Separation Logic.

Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, and proving their soundness is non-trivial. This paper shows that the complication is in principle unnecessary. In particular, we show that plain old parametric polymorphism, as found in Haskell, is all that is needed. We substantiate this claim by giving a type- and meaning-preserving translation from a variation of the region calculus of Tofte and Talpin to a monadic variant of System F with region primitives whose types and operations are inspired by (and generalize) the ST monad of Launchbury and Peyton Jones.

A precise characterization of those security policies enforceable by program rewriting is given. This also exposes and rectifies problems in prior work, yielding a better characterization of those security policies enforceable by execution monitors as well as a taxonomy of enforceable security policies. Some but not all classes can be identified with known classes from computational complexity theory.

The concept of a “unique” object arises in many emerging programming languages such as Clean, CQual, Cyclone, TAL, and Vault. In each of these systems, unique objects make it possible to perform operations that would otherwise be prohibited (e.g., deallocating an object) or to ensure that some obligation will be met (e.g., an opened file will be closed). However, different languages provide different interpretations of “uniqueness” and have different rules regarding how unique objects interact with the rest of the language. Our goal is to establish a common model that supports each of these languages, by allowing us to encode and study the interactions of the different forms of uniqueness. The model we provide is based on a substructural variant of the polymorphic λ-calculus, augmented with four kinds of mutable references: unrestricted, relevant, affine, and linear. The language has a natural operational semantics that supports deallocation of references, strong (type-varying) updates, and storage of unique objects in shared references. We establish the strong soundness of the type system by constructing a novel, semantic interpretation of the types. This technical report is really two documents in one: The first part is a paper appearing in the Tenth ACM SIGPLAN International Conference on Functional Programming (ICFP’05). The second part is a formal development of the language, step-indexed model, and soundness proof referenced in the first part. If you have already read a version of “A Step-Indexed Model of Substructural State”, then you should proceed directly to the appendices.

Concepts and techniques from modern programming languages have much to offer to the security of computer systems. This special issue is devoted to research on those concepts and techniques. Over 60 active researchers working in this area were invited to contribute. In particular, a number of the participants of the Dagstuhl Seminar on Language-Based Security were encouraged to submit. Submitted articles were reviewed by 3–4 referees. As a result of the reviewing process, five articles were selected for inclusion in the special issue.

Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, so proving their soundness is non-trivial. This paper shows that the complication is in principle unnecessary. In particular, we show that plain old parametric polymorphism, as found in Haskell, is all that is needed. We substantiate this claim by giving a type- and meaning-preserving translation from a region-based language based on core Cyclone to a monadic variant of System F with region primitives whose types and operations are inspired by (and generalize) the ST monad.

The goal of the Cyclone project is to investigate type safety for low-level languages such as C. Our most difficult challenge has been providing programmers control over memory management while retaining type safety. This paper reports on our experience trying to integrate and effectively use two previously proposed, type-safe memory management mechanisms: statically-scoped regions and unique pointers. We found that these typing mechanisms can be combined to build alternative memory-management abstractions, such as reference counted objects and arenas with dynamic lifetimes, and thus provide a flexible basis. Our experience---porting C programs and building new applications for resource-constrained systems---confirms that experts can use these features to improve memory footprint and sometimes to improve throughput when used instead of, or in combination with, conservative garbage collection.

Proof-carrying code (PCC) was introduced by George Necula and Peter Lee in 1996. The principle is simple: we can eliminate the need to trust code by forcing the producer to give us a formal, machine-checkable proof that the code won't exhibit some "bad behavior" when executed. Thus, instead of having to perform a complicated (and thus un-trustworthy) analysis to determine whether or not code is bad, we can instead use a simple (and thus trustworthy) proof checker.The attraction to systems people was that the PCC frame-work placed no inherent limits on good code. As long as you could manufacture a proof that the code wasn't bad, then the code would be accepted. So, at least in principle, you wouldn't have to pay a performance penalty for safety. Over the past eight years, many researchers have worked to make PCC a reality. But I would argue that we are still very far from reaping the benefits that the framework promises. Good progress has been made in some areas, but there are a number of hard problems that remain. The hardest conceptual questions are (a) "What policies should we enforce?" and (b) "How does the code producer generate a proof?

Proof-carrying code (PCC) was introduced by George Necula and Peter Lee in 1996. The principle is simple: we can eliminate the need to trust code by forcing the producer to give us a formal, machine-checkable proof that the code won't exhibit some bad behavior when executed. Thus, instead of having to perform a complicated (and thus un-trustworthy) analysis to determine whether or not code is bad, we can instead use a simple (and thus trustworthy) proof checker.The attraction to systems people was that the PCC framework placed no inherent limits on good code. As long as you could manufacture a proof that the code wasn't bad, then the code would be accepted. So, at least in principle, you wouldn't have to pay a performance penalty for safety. Over the past eight years, many researchers have worked to make PCC a reality. But I would argue that we are still very far from reaping the benefits that the framework promises. Good progress has been made in some areas, but there are a number of hard problems that remain. The hardest conceptual questions are (a) What policies should we enforce? and (b) How does the code producer generate a proof?

This issue of the Journal of Functional Programming marks a point of transition. Our long-time Chief Editors, Simon Peyton Jones and Philip Wadler, are stepping down. Most of us are aware of the amazing research contributions that Simon and Phil have made to functional programming. But you may not be aware how much these two have put in behind the scenes.

The following three figures (figures 10, 11 and 12) were not shown in the original published version of the article. These figures constitute the entire static semantics of the STAL type system.

Cyclone is a type-safe programming language that provides explicit run-time code generation. The Cyclone compiler uses a template-based strategy for run-time code generation in which pre-compiled code fragments are stitched together at run time. This strategy keeps the cost of code generation low, but it requires that optimizations, such as register allocation and code motion, are applied to templates at compile time. This paper describes a principled approach to implementing such optimizations. In particular, we generalize standard flow-graph intermediate representations to support templates, define a mapping from (a subset of) Cyclone to this representation, and describe a dataflow-analysis framework that supports standard optimizations across template boundaries.

Cyclone [1, 2] is an experimental, type-safe programming language based upon the syntax, semantics, and spirit of C. The primary goal of the language is to provide a type-safe environment that is close enough to C in both appearance and functionality, that systems programmers will find it attractive and useful.The most challenging aspect of the design is capturing the spirit of C without compromising type-safety. In particular, systems programmers expect to have good control over data representations, memory management, and performance. Yet, these features are usually absent from high-level, type-safe languages (e.g., Java). Another challenge is validating a sufficiently wide set of idioms that are in fact type-safe, but which conventional type systems reject.To address these issues, we have used a novel combination of typing features in conjunction with some interesting inference and dataflow techniques. The most novel typing feature is the support for region-based memory management which was summarized in an earlier paper [1]. However, this paper did not discuss the inference techniques we use to validate the regions and effects.In this talk, I will briefly summarize the Cyclone type system and then focus on the analysis issues that arise in its implementation, including (a) kind and type inference, (b) region and effect inference, and (c) dataflow analysis for validating initialization, array subscripts, and linear pointers.

Cyclone is a type-safe programming language derived from C. The primary design goal of Cyclone is to let programmers control data representation and memory management without sacrificing type-safety. In this paper, we focus on the region-based memory management of Cyclone and its static typing discipline. The design incorporates several advancements, including support for region subtyping and a coherent integration with stack allocation and a garbage collector. To support separate compilation, Cyclone requires programmers to write some explicit region annotations, but a combination of default annotations, local type inference, and a novel treatment of region effects reduces this burden. As a result, we integrate C idioms in a region-based framework. In our experience, porting legacy C to Cyclone has required altering about 8% of the code; of the changes, only 6% (of the 8%) were region annotations.

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling and attened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks: it requires duplication of run-time constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion. We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place, thereby avoiding certain beta-expansions required by other frameworks.

This paper presents STAL, a variant of Typed Assembly Language with constructs and types to support a limited form of stack allocation. As with other statically-typed low-level languages, the type system of STAL ensures that a wide class of errors cannot occur at run time, and therefore the language can be adapted for use in certifying compilers where security is a concern. Like the Java Virtual Machine Language (JVML), STAL supports stack allocation of local variables and procedure activation records, but unlike the JVML, STAL does not pre-suppose fixed notions of procedures, exceptions, or calling conventions. Rather, compiler writers can choose encodings for these high-level constructs using the more primitive RISC-like mechanisms of STAL. Consequently, some important optimizations that are impossible to perform within the JVML, such as tail call elimination or callee-saves registers, can be easily expressed within STAL.

Software developers often structure programs in such a way that different pieces of code constitute distinct principals . Types help define the protocol by which these principals interact. In particular, abstract types allow a principal to make strong assumptions about how well-typed clients use the facilities that it provides. We show how the notions of principals and type abstraction can be formalized within a language. Different principals can know the implementation of different abstract types. We use additional syntax to track the flow of values with abstract types during the evaluation of a program and demonstrate how this framework supports syntactic proofs (in the sytle of subject reduction) for type-abstraction properties. Such properties have traditionally required semantic arguments; using syntax aboids the need to build a model and recursive typesfor the language. We present various typed lambda calculi with principals, including versions that have mutable state and recursive types.

Region-based memory management is an alternative to standard tracing garbage collection that makes operation such as memory deallocation explicit but verifiably safe. In this article, we present a new compiler intermediate language, called the Capability Language (CL), that supports region-based memory management and enjoys a provably safe type systems. Unlike previous region-based type system, region lifetimes need not be lexically scoped, and yet the language may be checked for safety without complex analyses. Therefore, our type system may be deployed in settings such as extensible operating systems where both the performance and safety of untrusted code is important. The central novelty of the language is the use of static capabilities to specify the permissibility of various operations, such as memory access and deallocation. In order to ensure capabilities are relinquished properly, the type system tracks aliasing information using a form of bounded quantification. Moreover, unlike previous work on region-based type systems, the proof of soundness of our type system is relatively simple, employing only standard syntactic techniques. In order to show how our language may be used in practice, we show how to translate a variant of Tofte and Talpin's high-level type-and-effects system for region-based memory management into our language. When combined with known region inference algorithms, this translation provides a way to compile source-level languages to CL.

Programs are often structured around the idea that di#erent pieces of code comprise distinct principals, each with a view of its environment. Typical examples include the modules of a large program, a host and its clients, or a collection of interactive agents. In this paper, we formalize this notion of principal in the programming language itself. The result is a language in which intuitive statements such as, "the client must call open to obtain a file handle" can be phrased and proven formally. We add principals to variants of the simply-typed #-calculus and show how we can track the code corresponding to each principal throughout evaluation. We use this multiagent calculus to give syntactic proofs of some type abstraction properties that traditionally require semantic arguments. 1 Introduction Programmers often have a notion of principal in mind when designing the structure of a program. Examples of such principals include modules of a large system, a host and its clients, and, ...

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 collection by making memory management explicit but verifiably safe. However, it has not been clear how to use regions in low-level, type-safe code. We present a compiler intermediate language, called the Capability Calculus, that supports region-based memory management, enjoys a provably safe type system, and is straightforward to compile to a typed assembly language. Source languages may be compiled to our language using known region inference algorithms. Furthermore, region lifetimes need not be lexically scoped in our language, yet the language may be checked for safety without complex analyses. Finally, our soundness proof is relatively simple, employing only standard techniques.

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 ideas of Cardelli, and module constructs from high-level languages, we present a formal model of typed object files and a set of inference rules that are sufficient to guarantee that type safety is preserved by the linking process.\n\nWhereas Cardelli's link calculus is built on top of the simply-typed lambda calculus, our object files are based upon typed assembly language so that we may model important low-level implementation issues. Furthermore, unlike Cardelli, we provide support for abstract types and higher-order type constructors - features critical for building extensible systems or modern programming languages such as ML.

We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks: it requires duplication of constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion.We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place thereby avoiding certain beta-expansions required by other frameworks.

The challenge is to develop an easily usable protocol development framework that combines the flexibility of layered implementations, the efficiency of tightly-coupled monolithic implementations and the correctness achievable using high-level protocol validation languages. This challenge is addressed by a language-based framework that introduces a new protocol specification language called Promela++. The framework consists of a protocol verification tool and an optimizing compiler that generates efficient protocol code from Promela++ specifications. Promela++ is based on the Promela protocol validation language and has been designed with a rich set of domain-specific constructs. These constructs facilitate the task of protocol specification as well as enable the Promela++ compiler to perform domain-specific optimizations. The Promela++ compiler can also automatically transform protocol specifications in Promela++ to protocol models in Promela. The article presents a new language that unites the twin goals of checking protocol correctness using model checkers, and efficient protocol construction using optimizing compilers, under a single framework; exploits language design to provide mechanisms that simultaneously ease programming and enable generation of efficient protocol code; and demonstrates the effectiveness of this approach by doing a complete evaluation of multiple protocol implementations in Promela++.

Many high-level language compilers generate C code and then invoke a C compiler for code generation. To date, most, of these compilers link the resulting code against a conservative mark-sweep garbage collector in order to reclaim unused memory. We introduce a new collector, MCC, based on an extension of mostly-copying collection.We analyze the various design decisions made in MCC and provide a performance comparison to the most widely used conservative mark-sweep collector (the Boehm-Demers-Weiser collector). Our results show that a good mostly-copying collector can outperform a mature highly-optimized mark-sweep collector when physical memory is large relative to the live data. A surprising result of our analysis is that cache behavior can have a greater impact on overall performance than either collector time or allocation time.

We motivate the design of a statically typed assembly language (TAL) and present a type-preserving translation from System F to TAL. The TAL we present is based on a conventional RISC assembly language, but its static type system provides support for enforcing high-level language abstractions, such as closures, tuples, and objects, as well as user-defined abstract data types. The type system ensures that well-typed programs cannot violate these abstractions. In addition, the typing constructs place almost no restrictions on low-level optimizations such as register allocation, instruction selection, or instruction scheduling.Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly language provide a fully automatic way to produce proof carrying code, suitable for use in systems where untrusted and potentially malicious code must be checked for safety before execution.

article Free Access Share on TIL: a type-directed optimizing compiler for ML Authors: D. Tarditi School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PAView Profile , G. Morrisett School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PAView Profile , P. Cheng School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PAView Profile , C. Stone School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PAView Profile , R. Harper School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PAView Profile , P. Lee School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PAView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 31Issue 5May 1996 pp 181–192https://doi.org/10.1145/249069.231414Online:01 May 1996Publication History 212citation719DownloadsMetricsTotal Citations212Total Downloads719Last 12 Months39Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Closure conversion is a program transformation used by compilers to separate code from data. Previous accounts of closure conversion use only untyped target languages. Recent studies show that translating to typed target languages is a useful methodology for building compilers, because a compiler can use the types to implement efficient data representations, calling conventions, and tag-free garbage collection. Furthermore, type-based translations facilitate security and debugging through automatic type checking, as well as correctness arguments through the method of logical relations.We present closure conversion as a type-directed, and type-preserving translation for both the simply-typed and the polymorphic λ-calculus. Our translations are based on a simple "closures as objects" principle: higher-order functions are viewed as objects consisting of a single method (the code) and a single instance variable (the environment). In the simply-typed case, the Pierce-Turner model of object typing where objects are packages of existential type suffices. In the polymorphic case, more careful tracking of type sharing is required. We exploit a variant of the Harper-Lillibridge "translucent type" formalism to characterize the types of polymorphic closures.

The views and conclusions contained in this document are those of the authors and should not be interpreted as

\Ve describe the design of a transaction facilit y for a language that supports higher-order functions.tVe factor transactions into four separable features: persistence, undoability, locking, and threads.Then, relying on function composition, we show how we can put them together again.Our modular approach toward building transactions enables us to construct a model of concurrent, nested, multi threaded transactions, as well as other nontradi tional models where not all features of traditional transactions are present.Key to our approach is the use of higher-order functions to make transactions first-class.Not only do we get clean composability of transactional features, but also we avoid the need to introduce special control General

We have built a portable platform for running Standard ML of New Jersey programs on multiprocessors. It can be used to implement user-level thread packages for multiprocessors within the ML language with first-class continuations. The platform supports experimentation with different thread scheduling policies and synchronization constructs. it has been used to construct a Modula-3 style thread package and a version of Concurrent ML, and has been ported to three different multiprocessors running variants of Unix. This paper describes the platform's design, implementation, and performance.