Network processors generated huge excitement, interest and investment in the late 90's and into 2000, promising to replace fixed-function ASIC chips in networking equipment by high-performance programmable devices. The sheer performance requirements of these devices led to a flurry of activity in both processor architecture, software and especially the interaction between architecture and software, with many diverse approaches competing for survival. The subsequent collapse of the market for communications equipment hit network processors hard.This talk will give a progress report on network processors and embedded network processing elements. We begin by describing the application requirements for these computing devices and outline some of the processing tasks required - packet reassembly, classification, policing, statistics, state management, packet modification, queuing, scheduling and traffic shaping, buffer management, and packet segmentation - and their memory and I/O needs. We will then discuss how these requirements impact processor architecture, programming models and languages, and partitioning between software and hardware functionality, drawing examples from several of the network processor survivors. We will conclude with a market outlook for network processors, the impact that will likely have on future developments, and open research problems.

CRYPTONITE is a programmable processor tailored to the needs of crypto algorithms. The design of CRYPTONITE was based on an in-depth application analysis in which standard crypto algorithms (AES, DES, MD5, SHA-1, etc) were distilled down to their core functionality. We describe this methodology and use AES as a central example. Starting with a functional description of AES, we give a high level account of how to implement AES efficiently in hardware, and present several novel optimizations (which are independent of CRYPTONITE).We then describe the CRYPTONITE architecture, highlighting how AES implementation issues influenced the design of the processor and its instruction set. CRYPTONITE is designed to run at high clock rates and be easy to implement in silicon while providing a significantly better performance/area/power tradeoff than general purpose processors.

We consider the implication of deep sub-micron VLSI technology on the design of communication frameworks for parallel DSP systems-on-chip. We assert that distributed data transfer and control mechanisms are necessary to manage many independent processing subsystems and software tasks. An example of a parallel DSP architecture is given and used to demonstrate these mechanisms at work. We show the similarity of these mechanism and those used in large scale computing networks.

Known algorithms for pointer analysis are “global” in the sense that they perform an exhaustive analysis of a program or program component. In this paper we introduce a demand-driven approach for pointer analysis. Specifically, we describe a demand-driven flow-insensitive, subset-based, con text-insensitive points-to analysis. Given a list of pointer variables (a query), our analysis performs just enough computation to determine the points-to sets for these query variables. Using deductive reachability formulations of both the exhaustive and the demand-driven analyses, we prove that our algorithm is correct. We also show that our analysis is optimal in the sense that it does not do more work than necessary. We illustrate the feasibility and efficiency of our analysis with an implementation of demand-driven points-to analysis for computing the call-graphs of C programs with function pointers. The performance of our system varies substantially across benchmarks - the main factor is how much of the points-to graph must be computed to determine the call-graph. For some benchmarks, only a small part of the points-to graph is needed (e.g pouray emacs and gcc), and here we see more than a 10x speedup. For other benchmarks (e.g. burlap and gimp), we need to compute most (> 95%) of the points-to graph, and here the demand-driven algorithm is considerably slower, because using the demand-driven algorithm is a slow method of computing the full points-to graph.

We describe the design and implementation of a system for very fast points-to analysis. On code bases of about million lines of unpreprocessed C code, our system performs field-based Andersen-style points-to analysis in less than a second and uses less than 10MB of memory. Our two main contributions are a database-centric analysis architecture called compile-link-analyze (CLA), and a new algorithm for implementing dynamic transitive closure. Our points-to analysis system is built into a forward data-dependence analysis tool that is deployed within Lucent to help with consistent type modifications to large legacy C code bases.

We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis.

We show how to translate the region calculus of M. Tofte and J.P. Talpin (1997), a typed lambda calculus that can statically delimit the lifetimes of objects, into an extension of the polymorphic lambda calculus called F/sub #/. We give a denotational semantics of F/sub #/, and use it to give a simple and abstract proof of the correctness of memory deallocation.

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 translations help clarify aspects of the source calculi. We also define a semantic model for DCC and use it to give simple proofs of noninterference results for each case.

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 flow-of-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 power.

We define a general notion of set-based analysis --- any language whose operational semantics is defined by environment evaluation has a well defined set-based abstraction. This general definition covers both Aiken and Wimmers' type system and Heintze' set-based analysis. Aiken and Wimmers give a nondeterministic exponential time algorithm for their analysis. Heintze gives an O(n3) procedure. We show that this discrepancy is due to the complexity of the case statements analyzed. For polymorphic programs with deep patterns in case statements (as in the Aiken-Wimmers language) we show that the problem of determining type-safety under set-based abstraction is complete for deterministic exponential time. The problem remains complete for deterministic exponential time for programs without let (monovariant programs). However, for monovariant programs in which all patterns in case statements are shallow, as in the Heintze language, type-safety under set-based abstraction is decidable in cubic time. We give five additional theorems which (nearly exhaustively) characterize the time complexity of set-based analysis as a function of the complexity of case statements.

We prove that certain data-flow and control-flow problems are 2NPDA-complete. This means that these problems are in the class 2NPDA and that they are hard for that class. The fact that they are in 2NPDA demonstrates the richness of the class. The fact that they are hard for 2NPDA can be interpreted as evidence they can not be solved in sub-cubic time-the cubic time decision procedure for an arbitrary 2NPDA problem has not been improved since its discovery in 1968.

We present a linear-time algorithm for bounded-type programs that builds a directed graph whose transitive closure gives exactly the results of the standard (cubic-time) Control-Flow Analysis (CFA) algorithm. Our algorithm can be used to list all functions calls from all call sites in (optimal) quadratic time. More importantly, it can be used to give linear-time algorithms for CFA-consuming applications such as:• effects analysis: find the side-effecting expressions in a program.• k-limited CFA: for each call-site, list the functions if there are only a few of them (≤ k) and otherwise output "many".• called-once analysis: identify all functions called from only one call-site.

The paper develops a foundation for reasoning about protocol security. We adopt a model-based approach for defining protocol security properties. This allows us to describe security properties in greater detail and precision than previous frameworks. Our model allows us to reason about the security of protocols, and considers issues of beliefs of agents, time, and secrecy. We prove a composition theorem which allows us to state sufficient conditions on two secure protocols A and B such that they may be combined to form a new secure protocol C. Moreover, we give counter-examples to show that when the conditions are not met, the protocol C may not be secure.

We give a formal model of protocol security. The model allows us to reason about the security of protocol, and considers issues of beliefs of agents, time, and secrecy. We prove a composition theorem which allows us to state sufficient conditions on two secure protocols A and B such that they may be combined to form a new secure protocol C. Moreover, we give counter-examples to show that when the conditions are not met, the protocol C may not be secure.>

An engine that is based on unfolding of semantic equations is presented. A main advantage of the unfolding engine is a uniform treatment of structural information in a program. In particular, reasoning about partially instantiated structures, an area where traditional algorithms have been weak, is greatly enhanced. It is shown that the engine is uniformly more accurate than the standard engine in the sense that, given an abstract domain, its output, for any program is more accurate than that of the standard engine.>

A set constraint is of the form exp/sub 1/ contains exp/sub 2/ where exp/sub 1/ and exp/sub 2/ are set expressions constructed using variables, function symbols, projection symbols, and the set union, intersection, and complement symbols. While the satisfiability problem for such constraints is open, restricted classes have been useful in program analysis. The main result is a decision procedure for definite set constraints which are of the restricted form a contains exp, where a contains only constants, variables, and function symbols, and exp is a positive set expression (that is, it does not contain the complement symbol). A conjunction of such constraints, whenever satisfiable, has a least model and the algorithm will output an explicit representation of this model. An additional feature of the algorithm is that it deals with another important class of set constraints. These are the solved form set constraints which have the form X/sub 1/=exp/sub 1/, . . ., X/sub n/=exp/sub n/, where the X/sub i/ are distinct variables and the exp/sub i/ are positive set expressions. A solved form constraint is always satisfiable and possesses a least and a greatest model. The algorithm can output explicit representations of both.>

The notion of Cartesian closure on a set of unifiers has been used to define approximations of the least models of logic programs. Such approximations, often called types, are not known to be recursive. In this paper, we use Cartesian closure to define a similar, but more accurate, approximation. The main result proves that our approximation is not only recursive, but that it can be finitely represented in the form of a cyclic term graph. This explicit representation can be used as a starting point for logic program analyzers.