Commodity I/O hardware often fails to separate I/O transfers of isolated OS and applications code. Even when using the best I/O hardware, commodity systems sometimes trade off separation assurance for increased performance. Remarkably, device firmware need not be malicious. Instead, any malicious driver, even if isolated in its own execution domain, can manipulate its device to breach I/O separation. To prevent such vulnerabilities with high assurance, a formal I/O separation model and its use in automatic generation of secure I/O kernel code is necessary.This paper presents a formal I/O separation model, which defines a separation policy based on authorization of I/O transfers and is hardware agnostic. The model, its refinement, and instantiation in the Wimpy kernel design, are formally specified and verified in Dafny. We then specify the kernel implementation and automatically generate verified-correct assembly code that enforces the I/O separation policies. Our formal modeling enables the discovery of heretofore unknown design and implementation vulnerabilities of the original Wimpy kernel. Finally, we outline how the model can be applied to other I/O kernels and conclude with the key lessons learned.

Suppose that a trustworthy program must be booted on a commodity system that may contain persistent malware. Establishing root of trust (RoT) ensures the system has all and only the content chosen by a trusted verifier or the verifier discovers unaccounted content, with high probability. Obtaining such an assurance is challenging because malware can survive in system states across repeated secure- and trusted-boot operations and act on behalf of a powerful remote adversary. I this presentation, I illustrate both the theoretical and practical challenges of RoT establishment unconditionally; i.e., without secrets, trusted hardware modules (e.g., TPMs, HSMs) or adversary computation bounds. I also illustrate the only unconditional solution to this problem known to date. Establishing root of trust forces the adversary to repeat the malware-insertion attack, perhaps at some added cost. However, the inherent size and complexity of commodity OS components (aka., the "giants") render them vulnerable to such successful attacks. In contrast, small and simple software components with rather limited function and high-assurance security properties (aka., the "wimps") can, in principle, be resistant to attack. Maintaining root of trust assures a user that a commodity computer's wimps are isolated from, and safely co-exist with, adversary-controlled giants. However, regardless how secure program isolation may be, I/O separation must also be achieved despite the pitfalls of commodity architectures that encourage I/O hardware sharing, not isolation. In this presentation, I also illustrate the challenges of I/O separation and present and approach that enables the co-existence secure wimps with insecure giants, via an example of a system implemented at CMU.

Private communication detection (PCD) is a traffic-analysis technique whereby an ordinary user of a communication network exploits side channels in end-point devices to observe the busy/idle activity status of targeted users. Correlations of users' activity status allows collection of communication records that reveal private relationships. PCD techniques have been demonstrated for a number of communication technologies, such as Wi-Fi and VoIP, and their effectiveness shown even when the communication network is private; i.e., it provides content confidentiality, flow anonymity, and user pseudonymity. In this paper, we present a mathematical model of PCD that captures the activity status of two targets in a private VoIP network, including the probing process of an attacker that aims to breach their communication anonymity. Using this model, we a) develop fundamental bounds on PCD accuracy; b) measure the anonymity leakage in terms of the amount of call record information obtained in an attack; and c) provide performance guarantees and compare the efficacy of different PCD countermeasures, such as resource randomization and use of firewalls.

We make a case for packet-replay suppression at the network layer, a concept that has been generally neglected. Our contribution is twofold. First, we demonstrate a new attack, the router-reflection attack, that can be launched using compromised routers. In this attack, a compromised router degrades the connectivity of a remote Internet region just by replaying packets. The attack is feasible even if all packets are attributed to their sources, i.e., source authentication is in place, and our evaluation shows that the threat is pervasive---candidate routers for compromise are in the order of hundreds or thousands. Second, we design an in-network mechanism for replay suppression. We start by showing that designing such a mechanism poses unsolved challenges and simple adaptations of end-to-end solutions are not sufficient. Then, we devise, analyze, and implement a highly efficient protocol that suppresses replayed traffic at the network layer without global time synchronization. Our software-router prototype can saturate a 10 Gbps link using only two CPU cores for packet processing.

Abstract In the past few years, we have witnessed a rise in the popularity of ride-hailing services (RHSs), an online marketplace that enables accredited drivers to use their own cars to drive ride-hailing users. Unlike other transportation services, RHSs raise significant privacy concerns, as providers are able to track the precise mobility patterns of millions of riders worldwide. We present the first survey and analysis of the privacy threats in RHSs. Our analysis exposes high-risk privacy threats that do not occur in conventional taxi services. Therefore, we propose PrivateRide, a privacy-enhancing and practical solution that offers anonymity and location privacy for riders, and protects drivers’ information from harvesting attacks. PrivateRide lowers the high-risk privacy threats in RHSs to a level that is at least as low as that of many taxi services. Using real data-sets from Uber and taxi rides, we show that PrivateRide significantly enhances riders’ privacy, while preserving tangible accuracy in ride matching and fare calculation, with only negligible effects on convenience. Moreover, by using our Android implementation for experimental evaluations, we show that PrivateRide’s overhead during ride setup is negligible. In short, we enable privacy-conscious riders to achieve levels of privacy that are not possible in current RHSs and even in some conventional taxi services, thereby offering a potential business differentiator.

We investigate k-connectivity in secure wireless sensor networks under the random pairwise key predistribution scheme with unreliable links. When wireless communication links are modeled as independent on-off channels, this amounts to analyzing a random graph model formed by intersecting a random K-out graph and an Erdös-Rényi graph. We present conditions on how to scale the parameters of this intersection model so that the resulting graph is k-connected with probability approaching to one (resp. zero) as the number of nodes gets large. The resulting zero-one law is shown to improve and sharpen the previous result on the 1-connectivity of the same model. We also provide numerical results to support our analysis.

A trusted display service assures the confidentiality and authenticity of content output by a security-sensitive application and thus prevents a compromised commodity operating system or application from surreptitiously reading or modifying the displayed output. Past approaches have failed to provide trusted display on commodity platforms that use modern graphics processing units (GPUs). For example, full GPU virtualization encourages the sharing of GPU address space with multiple virtual machines {\em without} providing adequate hardware protection mechanisms; e.g., address-space separation and instruction execution control. This paper proposes a new trusted display service that has a minimal trusted code base and maintains full compatibility with commodity computing platforms. The service relies on a GPU separation kernel that (1) defines different types of GPU objects, (2) mediates access to security-sensitive objects, and (3) emulates object whenever required by commodity-platform compatibility. The separation kernel employs a new address-space separation mechanism that avoids the challenging problem of GPU instruction verification without adequate hardware support. The implementation of the trusted-display service has a code base that is two orders of magnitude smaller than other similar services, such as those based on full GPU virtualization. Performance measurements show that the trusted-display overhead added over and above that of the underlying trusted system is fairly modest.

We investigate k-connectivity in secure wireless sensor networks under the random pairwise key predistribution scheme with unreliable links; a network is said to be k-connected if it remains connected despite the failure of any of its (k - 1) nodes or links. With wireless communication links modeled as independent on-off channels, this amounts to analyzing a random graph model formed by intersecting a random K-out graph and an Erdös-Rényi graph. We present conditions on how to scale the parameters of this intersection model so that the resulting graph is k-connected with probability approaching to one (resp. zero) as the number of nodes gets large. The resulting zero-one law is shown to improve and sharpen the previous result on the 1-connectivity of the same model. We also provide numerical results to support our analysis and show that even in the finite node regime, our results can provide useful guidelines for designing sensor networks that are secure and reliable.

We examine the side-channel information leakage in first-come-first-serve (FCFS) packet schedulers. In this setup, an attacker aims to learn the packet arrival pattern of a private user that shares a FCFS packet scheduler with him, using the queuing delay information of his own packets. Under an information-theoretic metric for information leakage, we identify the optimal non-adaptive strategy for a given average probe rate of the attacker and report upto 1000% increase in information leakage compared to the attack strategy analyzed in the literature with the same average probe rate. The search for optimal strategies is reduced to linear programming, implying that the discovery of such strategies is in the domain of a real-world attacker.

The Eschenauer-Gligor (EG) random key predistri-bution scheme has been widely recognized as a typical approach to secure communications in wireless sensor networks (WSNs). However, there is a lack of precise probability analysis on the reliable connectivity of WSNs under the EG scheme. To address this, we rigorously derive the asymptotically exact probability of k-connectivity in WSNs employing the EG scheme with unreliable links represented by independent on/off channels, where k-connectivity ensures that the network remains connected despite the failure of any (k-1) sensors or links. Our analytical results are confirmed via numerical experiments, and they provide precise guidelines for the design of secure WSNs that exhibit a desired level of reliability against node and link failures.

Random key graphs form a class of random intersection graphs that are naturally induced by the random key predistribution scheme of Eschenauer and Gligor for securing wireless sensor network (WSN) communications. Random key graphs have received much attention recently, owing in part to their wide applicability in various domains, including recommender systems, social networks, secure sensor networks, clustering and classification analysis, and cryptanalysis to name a few. In this paper, we study connectivity properties of random key graphs in the presence of unreliable links. Unreliability of graph links is captured by independent Bernoulli random variables, rendering them to be on or off independently from each other. The resulting model is an intersection of a random key graph and an Erdos-Renyi graph, and is expected to be useful in capturing various real-world networks; e.g., with secure WSN applications in mind, link unreliability can be attributed to harsh environmental conditions severely impairing transmissions. We present conditions on how to scale this model's parameters so that: 1) the minimum node degree in the graph is at least k and 2) the graph is k-connected, both with high probability as the number of nodes becomes large. The results are given in the form of zero-one laws with critical thresholds identified and shown to coincide for both graph properties. These findings improve the previous results by Rybarczyk on k-connectivity of random key graphs (with reliable links), as well as the zero-one laws by Yagan on one-connectivity of random key graphs with unreliable links.

We study the secure and reliable connectivity of wireless sensor networks. Security is assumed to be ensured by the random pairwise key predistribution scheme of Chan, Perrig, and Song, and unreliable wireless links are represented by independent ON/OFF channels. Modeling the network by an intersection of a random K-out graph and an Erdos-Rényi graph, we present scaling conditions (on the number of nodes n, the scheme parameter K, and the probability p of a wireless channel being on), such that the resulting graph contains no nodes with a degree less than k with high probability. Results are given in the form of zero-one laws with n getting large, and are shown to improve the previous results by Yagan and Makowski on the absence of isolated nodes (i.e., absence of nodes with degree zero) in the same model. Through simulations, the established zero-one laws are also shown to hold for the property of k-connectivity, i.e., the property that graph remains connected despite the deletion of any k - 1 nodes or edges.

How pervasive is the vulnerability to link-flooding attacks that degrade connectivity of thousands of Internet hosts? Are some geographic regions more vulnerable than others? Do practical countermeasures exist? To answer these questions, we introduce the notion of the routing bottlenecks and show that it is a fundamental property of Internet design; i.e., it is a consequence of route-cost minimizations. We illustrate the pervasiveness of routing bottlenecks in an experiment comprising 15 countries and 15 cities distributed around the world, and measure their susceptibility to scalable link-flooding attacks. We present the key characteristics of routing bottlenecks, including size, link type, and distance from host destinations, and suggest specific structural and operational countermeasures to link-flooding attacks. These countermeasures can be deployed by network operators without needing major Internet redesign.

The q-composite key predistribution scheme [2] is used prevalently for secure communications in large-scale wireless sensor networks (WSNs). Prior work [5], [13], [44] explores topological properties of WSNs employing the q-composite scheme for q = 1 with unreliable communication links modeled as independent on/off channels. In this paper, we investigate topological properties related to the node degree in WSNs operating under the q-composite scheme and the on/off channel model. Our results apply to general q and are stronger than those reported for the node degree in prior work even for the case of q being 1. Specifically, we show that the number of nodes with an arbitrary degree asymptotically converges to a Poisson distribution, present the asymptotic probability distribution for the minimum degree of the network, and establish the asymptotically exact probability for the property that the minimum degree is at least an arbitrary value. Numerical experiments confirm the validity of our analytical findings.

We study the secure and reliable connectivity of wireless sensor networks. Security is assumed to be ensured by the random pairwise key predistribution scheme of Chan, Perrig, and Song, and unreliable wireless links are represented by independent on/off channels. Modeling the network by an intersection of a random K-out graph and an Erdös-Rényi graph, we present scaling conditions (on the number of nodes, the scheme parameter K, and the probability of a wireless channel being on) such that the resulting graph contains no node with degree less than k with high probability, when the number of nodes gets large. Results are given in the form of a zero-one law and are shown to improve the previous results by Yağan and Makowski on the absence of isolated nodes (i.e., absence of nodes with degree zero). Via simulations, the established zero-one laws are shown to hold also for the property of k-connectivity; i.e., the property that graph remains connected despite the deletion of any k - 1 nodes or edges.

To be trustworthy, security-sensitive applications must be formally verified and hence small and simple, i.e., wimpy. Thus, they cannot include a variety of basic services available only in large and untrustworthy commodity systems, i.e., in giants. Hence, wimps must securely compose with giants to survive on commodity systems, i.e., rely on giants' services but only after efficiently verifying their results. This paper presents a security architecture based on a wimpy kernel that provides on-demand isolated I/O channels for wimp applications, without bloating the underlying trusted computing base. The size and complexity of the wimpy kernel are minimized by safely outsourcing I/O subsystem functions to an untrusted commodity operating system and exporting driver and I/O subsystem code to wimp applications. Using the USB subsystem as a case study, this paper illustrates the dramatic reduction of wimpy-kernel size and complexity, e.g., over 99% of the USB code base is removed. Performance measurements indicate that the wimpy-kernel architecture exhibits the desired execution efficiency.

We propose STRIDE, a new DDoS-resilient Internet architecture that isolates attack traffic through viable bandwidth allocation, preventing a botnet from crowding out legitimate flows. This new architecture presents several novel concepts including tree-based bandwidth allocation and long-term static paths with guaranteed bandwidth. In concert, these mechanisms provide domain-based bandwidth guarantees within a trust domain - administrative domains grouped within a legal jurisdiction with enforceable accountability; each administrative domain in the trust domain can then internally split such guarantees among its endhosts to provide (1) connection establishment with high probability, and (2) precise bandwidth guarantees for established flows, regardless of the size or distribution of the botnet outside the source and the destination domains. Moreover, STRIDE maintains no per-flow state on backbone routers and requires no key establishment across administrative domains. We demonstrate that STRIDE achieves these DDoS defense properties through formal analysis and simulation. We also show that STRIDE mitigates emerging DDoS threats such as Denial-of-Capability (DoC) [6] and N2 attacks [22] based on these properties that none of the existing DDoS defense mechanisms can achieve.

Large-scale botnet attacks against Internet links using low-rate flows cannot be effectively countered by any of the traditional rate-limiting and flow-filtering mechanisms deployed in individual routers. In this paper, we present a collaborative defense mechanism, called CoDef, which enables routers to distinguish low-rate attack flows from legitimate flows, and protect legitimate traffic during botnet attacks. CoDef enables autonomous domains that are uncontaminated by bots to collaborate during link flooding attacks and reroute their customers' legitimate traffic in response to requests from congested routers. Collaborative defense using multi-path routing favors legitimate traffic while limiting the bandwidth available to attack traffic at a congested link. We present CoDef's design and evaluate its effectiveness by exploring the domain-level path-diversity of the Internet and performing simulations under various traffic conditions.

Random key predistribution scheme of Eschenauer and Gligor (EG) is a typical solution for ensuring secure communications in a wireless sensor network (WSN). Connectivity of the WSNs under this scheme has received much interest over the last decade, and most of the existing work is based on the assumption of unconstrained sensor-to-sensor communications. In this paper, we study the k-connectivity of WSNs under the EG scheme with physical link constraints; k-connectivity is defined as the property that the network remains connected despite the failure of any (k - 1) sensors. We use a simple communication model, where unreliable wireless links are modeled as independent on/off channels, and derive zero-one laws for the properties that i) the WSN is k-connected, and ii) each sensor is connected to at least k other sensors. These zero-one laws improve the previous results by Rybarczyk on the k-connectivity under a fully connected communication model. Moreover, under the on/off channel model, we provide a stronger form of the zero-one law for the 1-connectivity as compared to that given by Yağan.

We present the Crossfire attack -- a powerful attack that degrades and often cuts off network connections to a variety of selected server targets (e.g., servers of an enterprise, a city, a state, or a small country) by flooding only a few network links. In Crossfire, a small set of bots directs low intensity flows to a large number of publicly accessible servers. The concentration of these flows on the small set of carefully chosen links floods these links and effectively disconnects selected target servers from the Internet. The sources of the Crossfire attack are undetectable by any targeted servers, since they no longer receive any messages, and by network routers, since they receive only low-intensity, individual flows that are indistinguishable from legitimate flows. The attack persistence can be extended virtually indefinitely by changing the set of bots, publicly accessible servers, and target links while maintaining the same disconnection targets. We demonstrate the attack feasibility using Internet experiments, show its effects on a variety of chosen targets (e.g., servers of universities, US states, East and West Coasts of the US), and explore several countermeasures.

Recent trends in public-key infrastructure research explore the tradeoff between decreased trust in Certificate Authorities (CAs), resilience against attacks, communication overhead (bandwidth and latency) for setting up an SSL/TLS connection, and availability with respect to verifiability of public key information. In this paper, we propose AKI as a new public-key validation infrastructure, to reduce the level of trust in CAs. AKI integrates an architecture for key revocation of all entities (e.g., CAs, domains) with an architecture for accountability of all infrastructure parties through checks-and-balances. AKI efficiently handles common certification operations, and gracefully handles catastrophic events such as domain key loss or compromise. We propose AKI to make progress towards a public-key validation infrastructure with key revocation that reduces trust in any single entity.

A general theory of trust in networks of humans and computers must be built on both a theory of behavioral trust and a theory of computational trust.1 This argument is motivated by increased participation of people in online social networking, crowdsourcing, human computation, and socio-economic protocols; e.g., protocols modeled by trust and gift-exchange games, norms-establishing contracts, and scams/deception. We illustrate a class of interactive social protocols that relies both on trustworthy properties of commodity systems2 (e.g., verifiable end-to-end trusted path) and participant trust, since on-line verification of protocol compliance is often impractical; e.g., it can lead to undecidable problems, co-NP complete test procedures, and user inconvenience. Trust is captured by participant preferences (i.e., risk and betrayal aversion) and beliefs in the trustworthiness of other protocol participants. Both preferences and beliefs can be enhanced whenever protocol non-compliance leads to punishment of untrustworthy participants; i.e., it seems natural that betrayal aversion can be decreased and belief in trustworthiness increased by properly defined punishment. Similarly, risk aversion can be decreased and trustworthiness increased by feasible recovery from participant non-compliance.

Call-record analysis is one of the oldest tools used in defense, law-enforcement, and business intelligence. For example, the NSA collected over 1.9 trillion call records between 2001 and 2004 [1]. A call-record database allows both single link (e.g., time, initiation, frequency of a call) and cluster analysis of calls in the temporal, spatial, and frequency domains. It can also indicate overlaps among different clusters, such as those obtained from different investigations, and similarity of clusters, such as those obtained when a group of targets changes their phone numbers but not their communication habits [10, 12].

A trusted path is a protected channel that assures the secrecy and authenticity of data transfers between a user's input/output (I/O) device and a program trusted by that user. We argue that, despite its incontestable necessity, current commodity systems do not support trusted path with any significant assurance. This paper presents a hyper visor-based design that enables a trusted path to bypass an untrusted operating-system, applications, and I/O devices, with a minimal Trusted Computing Base (TCB). We also suggest concrete I/O architectural changes that will simplify future trusted-path system design. Our system enables users to verify the states and configurations of one or more trusted-paths using a simple, secret less, hand-held device. We implement a simple user-oriented trusted path as a case study.

Private communication detection (PCD) enables an ordinary network user to discover communication patterns (e.g., call time, length, frequency, and initiator) between two or more private parties. Ordinary users have neither eavesdropping capabilities (e.g., the network may employ strong anonymity measures) nor legal authority (e.g., collection of call records---without any voice/data content---requires "national security letters") to collect private-communication records. Analysis of communication patterns between private parties has historically been a powerful tool used by intelligence, military, law-enforcement and business organizations as it can reveal the strength of tie between these parties. In this paper, we show that PCD is possible by ordinary users merely by sending packets to various network end-nodes (e.g., WiFi nodes) and analyzing the timing of their responses. We show that timing side channels, which are caused by distinct resource-contention responses when different applications run in end nodes, enable effective PCD despite network and proxy-generated noise (e.g., jitter, delays). We use a stochastic analysis to demonstrate how PCD exploits indirectly accessible, remote end-node resources, such as WiFi radio channels and computer keyboards in Instant Messaging. Similar analysis enables practical Sybil node detection.

Recent statistics show that the number of online shoppers are increasing where the majority of them use online recommendation systems for product/service reviews. Although online reviews are becoming increasingly important, consumers face two major challenges of usability and robustness when they make purchase decisions based on the available reviews. More specifically, usability issues arise when consumers need to be able to extract relevant information given a high volume of data with uncertainty due to high variance. For robustness, judging the degree of truthfulness of the available recommendations can be a daunting task for consumers. In this paper, we propose a post-purchase tracking system as an enhancement to current online recommendation systems by embracing a peer review process and ask each consumer to score the reviews that previous consumers have posted. Furthermore, we propose to visualize the peer review processes such that people find the recommendation systems more efficient and useful to learn information. Our preliminary user study results indicate that our post-purchase tracking system is a promising approach that can help online consumers determine what information to trust with high confidence.

Clear evidence indicates the existence of compromised routers in ISP and enterprise networks. Fault localization (FL) protocols enable a network to localize specific links of compromised routers sabotaging network data delivery and are recognized as an essential means to enhancing network availability in the face of targeted attacks. However, theoretically proven lower bounds have shown that secure FL protocols in the current network infrastructure inevitably incur prohibitive overhead. We observe the current limits are due to a lack of trust relationships among network nodes. We demonstrate that we can achieve much higher FL efficiency by leveraging trusted computing technology to design a trusted network-layer architecture, Tru eN et, with a small Trusted Computing Base (TCB). We intend Tru e N e t to serve as a case study that demonstrates trusted computing's ability in yielding tangible and measurable benefits for secure network protocol designs.

Network-layer capabilities offer strong protection against link flooding by authorizing individual flows with unforgeable credentials (i.e., capabilities). However, the capability-setup channel is vulnerable to flooding attacks that prevent legitimate clients from acquiring capabilities; i.e., in Denial of Capability (DoC) attacks. Based on the observation that the distribution of attack sources in the current Internet is highly non-uniform, we provide a router-level scheme that confines the effects of DoC attacks to specified locales or neighborhoods (e.g., one or more administrative domains of the Internet). Our scheme provides precise access guarantees for capability schemes, even in the face of flooding attacks. The effectiveness of our scheme is evaluated by ns2 simulations under different attack scenarios.

Malware-contaminated hosts organized as a “bot network” can target and flood network links (e.g., routers). Yet, none of the countermeasures to link flooding proposed to date have provided dependable link access (i.e., bandwidth guarantees) for legitimate traffic during such attacks. In this paper, we present a router subsystem called FLoc (Flow Localization) that confines attack effects and provides differential bandwidth guarantees at a congested link: (1) packet flows of uncontaminated domains (i.e., Autonomous Systems) receive better bandwidth guarantees than packet flows of contaminated ones, and (2) legitimate flows of contaminated domains are guaranteed substantially higher bandwidth than attack flows. FLoc employs new preferential packet-drop and traffic-aggregation policies that limit “collateral damage” and protect legitimate flows from a wide variety of flooding attacks. We present FLoc's analytical model for dependable link access, a router design based on it, and illustrate FLoc's effectiveness using simulations of different flooding strategies and comparisons with other flooding defense schemes.

Few of the system architectures for security proposed for the past four decades (e.g., fine-grain domains of protection, virtual machines) have made a significant difference on client-side security. In this presentation, I examine some of the reasons for this and some of the lessons learned to date. Focus on client-side security is warranted primarily because it is substantially more difficult to achieve than server security in practice, since clients interact with human users directly. I argue that system and application partitioning to meet user security needs is now feasible, and that special focus must be placed on how to design and implement trustworthy communication, not merely secure channels, between system partitions.

An important security challenge is to protect the execution of security-sensitive code on legacy systems from malware that may infect the OS, applications, or system devices. Prior work experienced a tradeoff between the level of security achieved and efficiency. In this work, we leverage the features of modern processors from AMD and Intel to overcome the tradeoff to simultaneously achieve a high level of security and high performance. We present TrustVisor, a special-purpose hypervisor that provides code integrity as well as data integrity and secrecy for selected portions of an application. TrustVisor achieves a high level of security, first because it can protect sensitive code at a very fine granularity, and second because it has a very small code base (only around 6K lines of code) that makes verification feasible. TrustVisor can also attest the existence of isolated execution to an external entity. We have implemented TrustVisor to protect security-sensitive code blocks while imposing less than 7% overhead on the legacy OS and its applications in the common case.

Summary form only given. Invariably, new technologies introduce new vulnerabilities which often enable new attacks by increasingly potent adversaries. Yet new systems are more adept at handling well-known attacks by old adversaries than anticipating new ones. Our adversary models seem to be perpetually out of date: often they do not capture adversary attacks and sometimes they address attacks rendered impractical by new technologies. In this panel presentation, I provide a brief overview of adversary models beginning with those required by program and data sharing technologies ('60-70s), continuing with those required by computer communication and networking technologies (70s-'90s), and ending with those required by and sensor network technologies ('00s ->). I argue that sensor, ad-hoc, and mesh networks require new models, that are able to account for physical node capture by adversaries. Protecting device secrets (e.g., cryptographic keys) via physical security mechanisms will continue to require network security measures, despite advances in physical security measures and devices. I argue that "good-enough" measures in the face of node capture by adversaries can be obtained by using emergent properties. Intuitively, these are properties that cannot be provided by individual network nodes - no matter how well-endowed nodes might be - but instead result from interaction and collaboration among multiple nodes. Such properties can be used to detect, often probabilistically, the presence of an adversary within a network and to pinpoint with reasonable accuracy the affected network area (e.g., identify a specific captured node, a particular properly of captured nodes). However, all such measures require periodic network monitoring in normal mode to detect a somewhat rare event (i.e., node capture, replica insertion) and hence their cost can be high. I illustrate a new simple probabilistic protocol that avoids the effects of node capture by detecting adversaries attempts to access a node's internal state, and discuss various design trade-offs that will characterize much of the future research in this area.

We argue that the traditional notion of trust as a relation among entities, while useful, becomes insufficient for emerging data-centric mobile ad hoc networks. In these systems, setting the data trust level equal to the trust level of the data- providing entity would ignore system salient features, rendering applications ineffective and systems inflexible. This would be even more so if their operation is ephemeral, i.e., characterized by short-lived associations in volatile environments. In this paper, we address this challenge by extending the traditional notion of trust to data-centric trust: trustworthiness attributed to node-reported data per se. We propose a framework for data-centric trust establishment: First, trust in each individual piece of data is computed; then multiple, related but possibly contradictory, data are combined; finally, their validity is inferred by a decision component based on one of several evidence evaluation techniques. We consider and evaluate an instantiation of our framework in vehicular networks as a case study. Our simulation results show that our scheme is highly resilient to attackers and converges stably to the correct decision.

Invariably, new technologies introduce new vulnerabilities which often enable new attacks by increasingly potent adversaries. Yet new systems are more adept at handling well-known attacks by old adversaries than anticipating new ones. Our adversary models seem to be perpetually out of date: often they do not capture adversary attacks and sometimes they address attacks rendered impractical by new technologies.In this talk, I provide a brief overview of adversary models beginning with those required by program and data sharing technologies ('60-'70s), continuing with those required by computer communication and networking technologies ('70s-'90s), and ending with those required by and sensor network technologies ('00s ->). I argue that sensor, ad-hoc, and mesh networks require new models, different from those in common use, namely those of the Dolev-Yao and Byzantine adversaries. I illustrate this with adversaries that attack perfectly sensible and otherwise correct protocols of sensor networks. These attacks cannot be countered with traditional security protocols using end-to-end design arguments and require emergent security properties as countermeasures.

Secure sensor network communication protocols need to provide three basic properties: data secrecy, authentication, and replay protection. Secure sensor network link layer protocols such as Tiny-Sec [10] and ZigBee [24] enjoy significant attention in the community. However, TinySec achieves low energy consumption by reducing the level of security provided. In contrast, ZigBee enjoys high security, but suffers from high energy consumption.

The seven papers in this special issue focus on developments in the area of vehicular networks.

A common characteristic of all ad-hoc networks is that of emergent properties. Intuitively, emergent properties are features that cannot be provided by individual network nodes themselves but instead result from interaction and collaboration among network nodes. In this talk, we present the salient characteristics of these properties and discuss their security implications. Several examples of emergent properties in sensor and ad-hoc networks are discussed including key connectivity, trust establishment, and node replica detection. We conclude with a common theme of current research in security of emergent properties, namely that of a new threat model whereby the adversary may adaptively compromise nodes of a network. We contrast this theme with that of past research that limits an adversary to "man-in-the-middle" attacks and relies exclusively on end-to-end security solutions.

In this paper we look at the problem of interoperability of digital rights management (DRM)systems in home networks. We introduce an intermediate module called the Domain Interoperability Manager (DIM) to efficiently deal with the problem of content and license translation across different DRM regimes. We also consider the threat model specific to interoperability systems, and introduce threats such as the cross-compliancy and splicing attacks. We formalize the adversary model and define security of an interoperable DRM system with respect to this adversary. We finalize by proposing detailed protocols which achieve our security requirements. In order to achieve these requirements we provide novel applications of recently proposed proxy resignature and proxy re-encryption algorithms.

The low-cost, off-the-shelf hardware components in unshielded sensor-network nodes leave them vulnerable to compromise. With little effort, an adversary may capture nodes, analyze and replicate them, and surreptitiously insert these replicas at strategic locations within the network. Such attacks may have severe consequences; they may allow the adversary to corrupt network data or even disconnect significant parts of the network. Previous node replication detection schemes depend primarily on centralized mechanisms with single points of failure, or on neighborhood voting protocols that fail to detect distributed replications. To address these fundamental limitations, we propose two new algorithms based on emergent properties (Gligor (2004)), i.e., properties that arise only through the collective action of multiple nodes. Randomized multicast distributes node location information to randomly-selected witnesses, exploiting the birthday paradox to detect replicated nodes, while line-selected multicast uses the topology of the network to detect replication. Both algorithms provide globally-aware, distributed node-replica detection, and line-selected multicast displays particularly strong performance characteristics. We show that emergent algorithms represent a promising new approach to sensor network security; moreover, our results naturally extend to other classes of networks in which nodes can be captured, replicated and re-inserted by an adversary.

Key management has two important aspects: key distribution, which describes how to disseminate secret information to the principals so that secure communications can be initiated, and key revocation, which describes how to remove secrets that may have been compromised. Key management in sensor networks face constraints of large scale, lack of a priori information about deployment topology, and limitations of sensor node hardware. While key distribution has been studied extensively in recent works, the problem of key and node revocation in sensor networks has received relatively little attention. Yet, revocation protocols that function correctly in the presence of active adversaries pretending to be legitimate protocol participants via compromised sensor nodes are essential. In their absence, an adversary could take control of the sensor network's operation by using compromised nodes which retain their network connectivity for extended periods of time. In this paper, we present an overview of key-distribution methods in sensor networks and their salient features to provide context for understanding key and node revocation. Then, we define basic properties that distributed sensor-node revocation protocols must satisfy and present a protocol for distributed node revocation that satisfies these properties under general assumptions and a standard attacker model.

To date, most solutions proposed for secure routing in mobile ad-hoc networks (MANETs), assume that secure associations between pairs of nodes can be established on-line; e.g., by a trusted third party, by distributed trust establishment. However, establishing such security associations, with or without trusted third parties, requires reliance on routing layer security. In this paper, we eliminate this apparent cyclic dependency between security services and secure routing in MANETs and show how to bootstrap security for the routing layer. We use the notion of statistically unique and cryptographically verifiable (SUCV) identifiers to implement a secure binding between IP addresses and keys that is independent of any trusted security service. We illustrate our solution with the dynamic source routing (DSR) protocol and compare it with other solutions for secure routing.

Distributed Sensor Networks (DSNs) are ad-hoc mobile networks that include sensor nodes with limited computation and communication capabilities. DSNs are dynamic in the sense that they allow addition and deletion of sensor nodes after deployment to grow the network or replace failing and unreliable nodes. DSNs may be deployed in hostile areas where communication is monitored and nodes are subject to capture and surreptitious use by an adversary. Hence DSNs require cryptographic protection of communications, sensor-capture detection, key revocation and sensor disabling. In this paper, we present a key-management scheme designed to satisfy both operational and security requirements of DSNs. The scheme includes selective distribution and revocation of keys to sensor nodes as well as node re-keying without substantial computation and communication capabilities. It relies on probabilistic key sharing among the nodes of a random graph and uses simple protocols for shared-key discovery and path-key establishment, and for key revocation, re-keying, and incremental addition of nodes. The security and network connectivity characteristics supported by the key-management scheme are discussed and simulation experiments presented.

We argue that joint administration of access policies for a dynamic coalition formed by autonomous domains requires that these domains set up a coalition authority that distributes attribute certificates authorizing access to policy objects (e.g., ACLs). Control over the issuance of such certificates is retained by member domains separately holding shares of the joint coalition authority's private key with which they sign the attribute certificates. Hence, any (proper) subset of the member domains need not be trusted to protect the private key. However, application servers that implement joint administration of access policies based on attribute certificates must trust all the signers of those certificates, namely all member domains of the coalition. To capture these trust relations we extend existing access control logics and show that the extensions are sound. To reason about joint administration of access policies, we illustrate an authorization protocol in our logic for accessing policy objects using threshold attribute certificates.

The concept of non-interference seeks to characterize the absence of information flows through a computer system. The intuition is startlingly simple. Suppose that we want to assert that no information may flow from user A to user B via the system S. We characterize this by asserting that B’s view of S is unchanged by any alteration in A’s behaviour. It is thus asserting that A can have no causal influence on B’s interactions with and observations of the system. Non-interference is such a simple and obvious characterization of MLS confidentiality that the security community is understandably reluctant to give it up. However, it has well known problems. First, in real systems high-level input interferes with low-level output all the time. High-level files can be encrypted, sanitized, or simply downgraded and sent on their way over low-level networks. Second, after fifteen years of trying, we still don’t have any consensus as to what is the “correct” nondeterministic formulation of it. Nondeterministic versions tend to be too weak (e.g., Nondeducibility), too strong (e.g., Noninference), too cumbersome (e.g., PNI and AFM), too limiting (e.g., the Roscoe, Woodcock, Wulf determinism approach) too Baroque (e.g., Restrictiveness), or some combination of the five. In [2] it is argued that, in a process algebraic setting, the characterization of non-interference reduces to characterizing the equivalence of certain processes. This in turn is a fundamental and difficult question of theoretical computer science and one to which there is no universally agreed answer. Thus it is not even clear whether a “correct”, Platonic notion of secrecy actually exists. Non-interference would seem to be a fundamental notion in information security. It could be argued that, if we cannot get the specification and verification of the absence of information flows right, we really don’t understand the foundations of our subject. On the other hand, it is such an abstract formulation that it seems remote from real concerns of security managers, policy makers and the developers of secure systems. Most “real” security policies are concerned with specifying who has access to what resources under what circumstances. Non-interference is never mentioned. Furthermore, non-interference is in practice impossible to realise in any real system: contention for resources etc render it infeasible. Even the so-called One-WayRegulators (e.g. the NRL Pump) allow some downward flow, albeit of low channel capacity. The study of non-interference arose from the need to understand why covert channels were possible, at a time when the only theoretical security models were access-control models, which were unable to explain them. The first wave of responses consisted of information flow models, which used the syntactic structure of statements to recognize possible flows, such as “indirect flow” from the condition of an if-then statement to variables that might be modified in its body. These models were found to overestimate flows. The second wave of models were the deterministic non-interference models, which were based on the notion of functional dependency. These models explained some covert channels, and found flows only where they really existed. Subsequent varieties of models found more channels by allowing for nondeterminacy in the computer system model, either “possibilistic” or probabilistic, and still other models addressed desirable features like composability. What’s wrong with these models? This question could be addressed at several levels. At the policy level, it has been suggested that no one cares about covert channels anymore, therefore models that purport to explain them are uninteresting. This does not really seem to be a valid response. There may be a shift in application areas, however. There is less emphasis in the design of multilevel operating systems, but more interest in something like the Bleichenbacher attack on the PKCS #1 cryptographic protocol standard [1], where a channel that is due partly to the algorithm and partly to the protocol design leads to compromise of encrypted data. Attacks that might expose a stored key are of great concern. The basic principles of information compromise still apply. There is also the practical question of how noninterference theory can be translated into efficient algorithms for detecting covert channels. Non-interference anal-

The author presents some highlights of two areas of operating systems security that figured prominently in some of the best research in the areas of security and privacy over the past twenty years (1980-99). He examines the following: reference monitors and trusted computing bases, and intrusion detection.

Formally defines a wide variety of separation-of-duty (SoD) properties, including the best known to date, and establishes their relationships within a formal model of role-based access control (RBAC). The formalism helps to remove all the ambiguities of informal definition and offers a wide choice of implementation strategies. We also explore the composability of SoD properties and policies under a simple criterion. We conclude that the practical implementation of SoD policies requires new methods and tools for security administration, even within applications that already support RBAC, such as most database management systems.

Operational security problems, which are often the result of access authorization misuse, can lead to intrusion in secure computer systems. We motivate the need for pattern-oriented intrusion detection, and present a model that tracks both data and privilege flows within secure systems to detect context-dependent intrusions caused by operational security problems. The model allows the uniform representation of various types of intrusion patterns, such as those caused by unintended use of foreign programs and input data, imprudent choice of default privileges, and use of weak protection mechanisms. As with all pattern-oriented models, this model cannot be used to detect new, unanticipated intrusion patterns that could be detected by statistical models. For this reason, we expect that this model will complement, not replace, statistical models for intrusion detection.

In this paper we investigate the illicit means of leaking sensitive or private information in operating systems. The leakage cannot be eliminated either by the use of access control and authentication mechanisms or by administrative measures since unauthorized access need not be attempted. In order to resolve the problem, we designed an audit system which is able to detect the illicit leakage of information. This audit system consists of two major components: an enhanced audit-collection mechanism and an audit-analysis tool.

The authors present a design method for message integrity protection. They illustrate the use of the method by designing large classes of message types whose integrity is provably preserved and by applying the method to the symmetric key option of the privacy-enhanced electronic mail protocol to help discover and eliminate an integrity vulnerability. The method is independent of the specific encryption system and checksum/digest functions used. It expresses desirable requirements for message integrity protection in terms of abstract encryption and checksum/digest properties, and relates these properties to the message type representation, and lifetime of the protocol run and keys used. The use of the method is illustrated by the design of a large class of message types whose integrity is provably preserved in the face of active intruder attacks. In particular, the method is used to help discover and eliminate a vulnerability in the symmetric-key option of the privacy-enhanced electronic mail (PEM) protocol for the internet.>

A multiuser relational database management system (DBMS), Trusted RUBIX, has been designed and implemented to satisfy the requirements of the TCSEC at the B2 class. The architecture of trusted RUBIX is presented, its integration within the B2 UNIX System V platform is discussed, and the adaptation and interpretation of the SeaViews security policy model in Trusted RUBIX are explained. The lessons learned from this design and implementation exercise are also discussed.>

A policy for propagation of authentication trust across realm boundaries is defined and rationalized. This policy helps limit global security exposures that ensue whenever an authentication service is compromised. The policy is based on a hierarchical model of inter-realm authentication and can be supported by both public key and secret key systems. As an example, a simple protocol which selects inter-realm authentication paths that satisfy the policy are presented. The protocol is part of a design which provides application transparency for inter-realm authentication path selection and acceptance as the default mode of operation. This design can be integrated with the security services of existing systems; e.g., of the Open Software Foundation's Distributed Computing Environment (DCE). DCE implementation issues are also discussed.>

An operational model for message integrity in cryptographic protocols is presented, message integrity requirements are discussed, and message structures that satisfy those requirements are suggested. A message splicing/decomposition invariant of the cipher block chaining (CBC) mode of encryption is derived and used to identify heretofore-unknown vulnerabilities of well-known protocols. The suggested message structures remove these vulnerabilities relying only on the use of weak one-way functions.>

A theoretical foundation for penetration analysis of computer systems is presented, which is based on a hypothesis and a set of formalized design properties that characterize penetration resistance. By separating the policy-enforcement mechanisms of

The authors discuss the virtues and limitations of several logics for cryptographic protocols focusing primarily on the logics of authentication. They emphasize the scope limitations of these logics rather than their virtues because: (1) their virtues to be better understood and accepted than their limitations; and (2) they hope to stimulate further research that will expand their scope.>

A theoretical foundation for penetration analysis of computer systems is presented, which is based on a set of formalized design properties that characterize resistance to penetration. By separating the policy-enforcement mechanisms of a system from the mechanisms necessary to protect the system itself, and by using a unified framework for representing a large set of penetration scenarios, the authors develop an extensible model for penetration analysis. Furthermore, they illustrate how the model is used to implement automated tools for penetration analysis. The theory, model, and tools only address system-penetration patterns caused by unprivileged users' code interactions with a system.>

Authentication protocols can be viewed from the perspective of the evolution of beliefs within a protocol run. Inference rules which ensue from this perspective are presented. These rules can be used to analyze the protocols which BAN logic can analyze. Additional protocols that can be analyzed include (1) interdomain authentication where principals must trust all authentication servers of the domains traversed according to a specific policy, and (2) where trust in the secrecy of the encryption key and belief ordering need to be established despite the lack of jurisdiction.>

Operational security problems can lead to intrusion in secure computer systems. The authors justify the need for, and present, a pattern-oriented intrusion-detection model that can be used to analyze object privilege and data flows in secure computer systems to detect operational security problems. This model can address context-dependent intrusion, such as use of covert-storage channels and virus propagation, and has been used to build an intrusion detection system for Trusted XENIX. Pattern-oriented intrusion detection is expected to complement, not replace, current statistical approaches to intrusion detection.>

Given an information flow consisting of the flow path and the flow condition under which the flow takes place, the problem of determining whether the information flow is legal is considered; that is, whether the flow complies with the underlying nondiscretionary security policy of a trusted computing base (TCB). It is shown that the proposed approach to information-flow analysis has the advantage of eliminating the possibility of generating false illegal flow, namely flows that are identified by the analysis process to be illegal but which, in reality, are legal. Without eliminating false illegal flows from analysis, automated tools for secure information-flow analysis would be of limited use in this area because manual work would still be needed. Finally, it is shown how to apply this information-flow analysis approach to Secure XENIX and how information-flow analysis can help reduce the amount of effort for information-flow integration within TCB programs.>

Various approaches to the problem of replay detection in distributed systems are briefly reviewed. An approach based on combining a variable-size time-window mechanism with a challenge mechanism is proposed. This approach has the following properties: (1) it does not depend on clock synchronization, (2) it allows the setting of a minimum server's memory-buffer size in a way that ensures acceptance of all legitimate client requests and (3) it is robust without requiring stable (nonvolatile) memory for the server buffer needed to save past client requests.>

The formal specification and verification of the multiparty session protocol discussed by the authors previously (1988) are presented. The notion of intruder processes is introduced to model intruder actions and countermeasures of the trusted computing bases. It is argued that multilevel network security can be achieved and verified formally independent of the specific transport-layer protocols even in the presence of intruders through the use of (1) a multilevel secure session protocol and (2) a key-distribution protocol which helps establish message confidentiality and integrity across an untrusted network. Both the formal security-policy model and the formal top-level specification (FTLS) of the multiparty session protocol are written in Ina Jo. The inference rules of the logic of authentication are incorporated in Ina Jo transforms to demonstrate the correctness of the key-distribution protocol. Two detailed examples of formal proofs are included.>

Requirements for auditing covert storage channels are defined, and some fundamental problems which appear in most computer systems are illustrated. It is argued that audit subsystems designed to minimally satisfy the TCSEC (the DoD Trusted Computer System Evaluation Criteria) requirement are unable to detect many instances of covert channel use, and hence require major design and implementation changes before they are able to detect all use of covert storage channels. The design of the Secure Xenix tool for covert-channel audit that has been in operation since July 1989 is presented. Results of experiments indicate that the tool is able to detect all use of covert storage channels without raising false alarms.>

A general protocol for atomic broadcast in networks is presented. The protocol tolerates loss, duplication, reordering, delay of messages, and network partitioning in an arbitrary network of fail-stop sites (i.e. no Byzantine site behavior is tolerated). The protocol is based on majority-concensus decisions to commit on unique ordering of received broadcast messages. Under normal operating conditions, the protocol requires three phases to complete and approximately 4N/V messages where N is the number of sites. This overhead is distributed among the messages of which the delivery decision is made and the heavier the broadcast message traffic, the lower the overhead per broadcast message becomes. Under abnormal operating conditions, a decentralized termination protocol (also presented) is invoked. A performance analysis of this protocol is presented, showing that this protocol commits with high probability under realistic operating conditions without invoking termination protocol if N is sufficiently large. The protocol retains its efficiency in wide-area networks where broadcast communication media are unavailable.>

A practical method for the identification of covert storage channels is presented and its application to the source code of the Secure Xenix kernel is illustrated. The method is based on the identification of all visible/alterable kernel variables by using information-flow analysis of language code. The method also requires that, after the sharing relationships among the kernel primitives and the visible/alterable variables are determined, the nondiscretionary access rules implemented by each primitive be applied to identify the potential storage channels. The method can be generalized to other implementation languages, and has the following advantages: it helps discover all potential storage channels is kernel code, thereby helping determine whether the nondiscretionary access rules are implemented correctly; it helps avoid discovery of false flow violations and their unnecessary analysis; and it helps identify the kernel locations where audit code and time-delay variables need to be placed for covert-channel handling.>

A specification and verification method is presented for preventing denial of service in absence of failures and of integrity violations. The notion of user agreements is introduced, and it is argued that lack of specifications for these agreements and for simultaneity conditions makes it impossible to demonstrate denial-of-service prevention, in spite of demonstrably fair service access. The use of this method is illustrated with an example and it is explained why current methods for specification and verification of safety and liveness properties of concurrent programs do not handle this problem. The proposed specification and verification method is meant to augment current methods for secure system design.>

A Markov model for bandwidth computation and its application to Secure Xenix are presented. The model can be used for computing the bandwidth of both individual channels and aggregated channels (i.e. serial and parallel aggregation). Using this model, a tool has been built and experiments conducted to determine the factors that affect the bandwidth of covert storage channels (noise, scheduling delays, load, etc.). The tool can be used to compute the minimum delays for each channel under various loads and program behavior. Thus, it allows the placement of dynamically adjustable delays in multiprogrammed systems, which guarantees minimum performance impact.>

The authors present a formal specification and verification method for the prevention of denial of service in absence of failures and integrity violations. They introduce the notion of user agreements and argue that lack of specifications for these agreements and for simultaneity conditions makes it impossible to demonstrate denial-of-service prevention, in spite of demonstrably fair service access. The authors illustrate the use of this method with two examples and explain why current methods for specification and verification of safety and liveness properties of concurrent programs have been unable to handle this problem. The proposed specification and verification method is meant to augment current methods for secure system design.>

A novel general protocol for atomic broadcast in networks is presented. The protocol tolerates loss, duplication, reordering, delay of messages, and network partitioning in an arbitrary network of 'fail-stop' sites (i.e. no Byzantine site behavior is tolerated). The protocol is fully decentralized and is based on majority-consensus decisions to commit on unique ordering of received broadcast messages. Under normal operating conditions, the protocol requires three phases to complete and approximately 4N messages where N is the number of sites. If more than 4N broadcast messages are exchanged in each protocol execution, this protocol achieves better performance than any of the protocols published to date without assuming specific types of site connectivity, clock synchronization, or knowledge of failed sites and failed communication links. Under abnormal operating conditions, a decentralized termination protocol, also presented, is invoked. A performance analysis of this protocol shows that it commits with high probability under realistic operating conditions without invoking termination protocol if N is sufficiently large.>

A formal method for the identification of covert storage channels is presented and its application to the source code of the Secure Xenix* kernel is illustrated. The method is based on the identification of all visible/alterable kernel variables by using information flow analysis of language code (e.g., C language code). The method also requires that, after the sharing relationships among the kernel primitives and the visible/ alterable variables are determined, the non-discretionary access rules implemented by each primitive be applied to identify the covert storage channels. The method can be generalized to other implementation languages, and has the following advantages: (1) it leads to the discovery of all storage channels in kernel implementations, (2) it helps determine whether the non-discretionary access rules are implemented correctly, and (3) it can be automated. An additional important aspect of applying this method to a kernel interface is the discovery of all kernel variables that are modified directly or indirectly through that interface. The analysis of the modification scenarios provides the necessary conditions for all kernel penetration. This implies that, in any kernel that enforces both a non-discretionary security and an integrity policy, penetration instances are the dual of covert storage channels instances.

Secure Xenix™ is an experimental system designed to run on IBM PC/AT workstations. Like Xenix, it is a Unix™ System V implementation on the PC/AT workstation; unlike Xenix, it eliminates the Unix security deficiencies and it enhances security policies. In this paper, we present the design features of Secure Xenix, their integration within Xenix, and some of the lessons learned from this experiment to date.

A new security testing method is proposed that combines the advantages of both traditional "black box" (monolithic functional) testing and "white box" (functional-synthesis-based) testing. The new method allows significant coverage both for security model-based tests and for individual kernel-call tests. It eliminates redundant kernel test cases 1) by using a variant of control synthesis graphs, 2) by analyzing dependencies between descriptive kernel-call specifications, and 3) by exploiting access check separability. A higher degree of test assurance is achieved than that of other security testing methods because the new method helps eliminate cyclic dependencies among test programs for different kernel calls. The application of this method to the testing of the Secure Xenix™ kernel is illustrated.

The problem of denial of service and some of Its properties are reviewed. Some common misconceptions about denial of service are explained. Although fundamental changes to the notion of denial of service are unwarranted by use of computer networks, new and novel Instances of the problem appear. Research directions for solutions to the denlal-of-servlce problem are suggested.

Secure Xenix * is an experimental system designed to run on IBM PC/AT workstations. Like Xenix, it is a Unix implementation on the PC/AT workstation; unlike Xenix, it eliminates the Unix security deficiencies and it enhances security policies. In this paper, we present the design features of Secure Xenix, their integration within Xenix, and some of the lessons learned from this experiment to date. In addition, we address some of the problems specific to workstations in the security management area. The major design differences between Secure Xenix and other experiments with Unix security enhancements, such as LINUS IV, are also presented. In a companion paper, we present the important problems that arise in the testing of Secure Xenix and their solutions.

A new security testing method is proposed that combines the advantages of both traditional "black box" (monolithic functional) testing and "white box" (functional-synthesis- based) testing. The new method allows significant coverage both for security model-based tests and for individual kernel-call tests. It eliminates redundant kernel test cases (1) by using a variant of control synthesis graphs, (2) by analyzing dependencies between descriptive kernel-call specifications, and (3) by exploiting access check separability. A higher degree of test assurance is achieved than that of other security testing methods because the new method helps eliminate cyclic dependencies among test programs for different kernel calls. The application of this method to the testing of the Secure Xenix* kernel is illustrated. The design and the implementation of Secure Xenix are presented in a companion paper.

An analysis of the verification approach used for the SCOMP hardware is presented herein. Although the SCOMP approach is informal it is extensive and thorough. In general, it provides sufficient evidence to conclude that the SCOMP hardware forms a sound basis for the development of a security kernel. However, the SCOMP approach presents a number of problems which are common to most informal verification approaches. These problems include: (1) incomplete formal top-level specification of the hardware functions that are visible at the TCB interface, and (2) incomplete coverage of design (and implementation) analysis and testing. The existence of verification problems does not imply that design/implementation flaws are left undiscovered and uncorrected in the SCOMP system. However, it does require that complete confidence in the hardware design (and implementation) be gained in alternate ways; e.g., by careful review of all possible implications of the verification omissions, and, possibly, by penetration analysis. All concerns raised along these lines with the system designers were answered in a satisfactory way.

THE concepts of system reliability–generally defined as the ability of a system to meet its interface specifications-and of system availability–generally defined as the ability of a system to meet its interface specifications within a specified time limit–predate not only that of distributed computing but also that of the electronic computer itself. With the advent of the electronic computer and its ever increasing penetration of technological, social, and political developments, reliability and availability gained additional recognition as disciplines of serious intellectual challenge. Much of the development of new reliability techniques can be linked directly to the computer hardware developments of the last three decades. However, until relatively recently, the concept of software reliability did not receive significant attention and, when it did, it was rather narrowly focused on approaches to prevent failures; i.e., on software development and verification methodologies, and on languages and tools.

A simple and general definition of denial-of-service in operating systems is presented. It is argued that no current protection mechanism nor model resolves this problem in any demonstrable way. The notion of interuser dependency is introduced and identified as the common cause for all problem instances. Decomposition of operating systems into hierarchies of services is assumed for the discovery of denial-of-service instances.

A simple and general definition of denial of service in operating systems is presented herein. It is argued that no current protection mechanism nor model resolves this problem in any demonstrable way. A set of examples from known systems is presented in order to delimit the scope of the problem. The notion of interuser dependency is introduced and identified as the common cause for all problem instances. Necessary end sufficient conditions for solutions are stated and justified informally. The relative complexity of undesirable (and unspecified) interuser dependencies is also discussed.

The problem of finding a minimum-cost, augmented-set basis is NP-complete. In this paper we show that this problem is not approximable. That is, if ${\text{P}} \ne {\text{NP}}$, then no constants c and d exist so that $A \leqq c{\text{ASB}} + d$, where A is the cost provided by a polynomial-time approximation algorithm and ASB is the optimal cost. We also provide a brief characterization of the cost functions for which this result remains valid. The proof technique used in the augmented-set basis problem is applied directly to other NP-complete problems, such as several graph augmentation and deletion problems, to show that they are also not approximable.

A hierarchically organized and a distributed protocol for deadlock detection in distributed databases are presented in [1]. In this paper we show that the distributed protocol is incorrect, and present possible remedies. However, the distributed protocol remains impractical because "condensations" of "transaction-wait-for" graphs make graph updates difficult to perform. Delayed graph updates cause the occurrence of false deadlocks in this as well as in some other deadlock detection protocols for distributed systems. The performance degradation that results from false deadlocks depends on the characteristics of each protocol.

Some protection mechanisms support the implementation of abstract type objects. The “separation of privilege” and the “least privilege” principles define several requirements that must guide the design of such protection mechanisms. Some of these requirements can be used to eliminate inadequate or unnecessary mechanisms. Type protection mechanisms and some of the requirements of the least privilege principle have either practical theoretical limitations. To mitigate these limitations, a capability-based architecture must support (1) the migration of abstract type objects outside the control of their type manager, and (2) inexpensive, small segments. To meet the requiements of the “separation of privilege” and “least privilege” principles, a capability-based architecture only needs to support (1) protected procedures and (2) “explicit” mechanisms for separating access privileges to objects and to object representations.

The problems of review and revocation of access privileges are presented in the context of the systems that use capabilities for the long-term distribution of access privileges. An approach that solves both of these problems in their-most general form is presented in this paper. The approach requires that a capability propagation graph be maintained in memory spaces associated with subjects (e.g., domains, processes, etc.) that make copies of the respective capability; the graph remains inaccessible to those subjects, however. Parallel processes of the operating system update the graph as the system runs.

When typed objects migrate in virtual memory, onto off-ine storage, or among the nodes of a network, the type managers must relinguish control over the object representation and state. In this paper we present a mechanism which allows a type manager to authenticate and reinstantiate migrated objects. This mechanism also solves some problems stemming from the hierarchical structure of the system itself. The mechanism is based on a combination of cryptographic techniques using (nondistributable) centralized, secret keys, and data redundancy which characterizes the object representation and state.