Administrators need effective tools to quickly and automatically obtain a succinct, yet informative, overview of the status of their networks to make critical administrative decisions in a timely and effective manner. While the existing tools might help in pointing out machines that are heavily used or services that are failing, more subtle relationships, such as indirect dependencies between services, are not made apparent. In this paper, we propose novel techniques to automatically provide insights into the state of a network and the importance of the network components. We developed a tool, called Paris, which receives traffic information from various off-the-shelf network monitoring devices. Paris computes an importance metric for the network's components based on which the administrators can prioritize their defensive and prohibitive actions. We evaluated Paris by running it on a mid-size, real-world network. The results show that Paris is able to automatically provide situation awareness in a timely, effective manner.

Detecting dependencies among network services has been well-studied in previous research. These attempts at service dependency detection fall into two classes: active and passive approaches. While passive approaches suffer from high false positives, active approaches suffer from applicability problems. In this paper, we design a new application-independent active approach for detecting dependencies among services. We present a traffic watermarking approach with arbitrarily low false positives and easy applicability. We provide statistical tests for detecting watermarked flows, and we compute the false positive and false negative rates of these tests both analytically and experimentally. Furthermore, we implemented the proposed watermarking system (Rippler) in a small university lab network. We ran our system for four months and detected 38 dependencies among 54 services. Finally, we compared the efficiency of our approach against three previous systems by testing them on this real-world network data.

Botnets, which are networks of malware-infected machines that are controlled by an adversary, are the root cause of a large number of security threats on the Internet. A particularly sophisticated and insidious type of bot is Torpig, which is a malware program that is designed to harvest sensitive information (such as bank account and credit card data) from its victims. In this talk, I report on our efforts to take control of the Torpig botnet for ten days. Over this period, we observed more than 180 thousand infections and recorded more than 70 GB of data that the bots collected.

Online advertisements (ads) provide a powerful mechanism for advertisers to effectively target Web users. Ads can be customized based on a user's browsing behavior, geographic location, and personal interests. There is currently a multi-billion dollar market for online advertising, which generates the primary revenue for some of the most popular websites on the Internet. In order to meet the immense market demand, and to manage the complex relationships between advertisers and publishers (i.e., the websites hosting the ads), marketplaces known as "ad exchanges" are employed. These exchanges allow publishers (sellers of ad space) and advertisers(buyers of this ad space) to dynamically broker traffic through ad networks to efficiently maximize profits for all parties. Unfortunately, the complexities of these systems invite a considerable amount of abuse from cybercriminals, who profit at the expense of the advertisers.

Electronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various e-voting systems show serious specification, design, and implementation flaws. The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties.This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations.

Voting is the process through which a democratic society determines its government. Therefore, voting systems are as important as other well-known critical systems, such as air traffic control systems or nuclear plant monitors. Unfortunately, voting systems have a history of failures that seems to indicate that their quality is not up to the task. Because of the alarming frequency and impact of the malfunctions of voting systems, in recent years a number of vulnerability analysis exercises have been carried out against voting systems to determine if they can be compromised in order to control the results of an election. We have participated in two such large-scale projects, sponsored by the Secretaries of State of California and Ohio, whose goals were to perform the security testing of the electronic voting systems used in their respective states. As the result of the testing process, we identified major vulnerabilities in all of the systems analyzed. We then took advantage of a combination of these vulnerabilities to generate a series of attacks that would spread across the voting systems and would “steal” votes by combining voting record tampering with social engineering approaches. As a response to the two large-scale security evaluations, the Secretaries of State of California and Ohio recommended changes to improve the security of the voting process. In this paper, we describe the methodology that we used in testing the two real-world electronic voting systems we evaluated, the findings of our analysis, our attacks, and the lessons we learned.

Botnets, networks of malware-infected machines that are controlled by an adversary, are the root cause of a large number of security problems on the Internet. A particularly sophisticated and insidious type of bot is Torpig, a malware program that is designed to harvest sensitive information (such as bank account and credit card data) from its victims. In this paper, we report on our efforts to take control of the Torpig botnet and study its operations for a period of ten days. During this time, we observed more than 180 thousand infections and recorded almost 70 GB of data that the bots collected. While botnets have been "hijacked" and studied previously, the Torpig botnet exhibits certain properties that make the analysis of the data particularly interesting. First, it is possible (with reasonable accuracy) to identify unique bot infections and relate that number to the more than 1.2 million IP addresses that contacted our command and control server. Second, the Torpig botnet is large, targets a variety of applications, and gathers a rich and diverse set of data from the infected victims. This data provides a new understanding of the type and amount of personal information that is stolen by botnets.

Recently, the use of formal methods to specify and verify properties of electronic voting (e-voting) systems, with particular interest in security, verifiability, and anonymity, is getting much attention. Formal specification and verification of such systems can greatly help to better understand the system requirements by thoroughly specifying and analyzing the underlying assumptions and security specific properties. Unfortunately, even though these systems have been formally verified to satisfy the desired system security requirements, they are still vulnerable to attack. In this paper we extend a formal specification of the ES&S voting system by specifying attacks that have been shown to successfully compromise the system. We believe that performing such analysis is important for two reasons: first, it allows us to discover some missing critical requirements for the specification and/or assumptions that were not met Second, it allows us to derive mitigation or counter-measure strategies when the system behaves differently than it should. We used the ASTRAL language for the specification, and the verification is performed using the PVS tool.

Electronic voting systems play a critical role in today's democratic societies, as they are responsible for recording and counting the citizens' votes. Unfortunately, there is an alarming number of reports describing the malfunctioning of these systems, suggesting that their quality is not up to the task. Recently, there has been a focus on the security testing of voting systems to determine if they can be compromised in order to control the results of an election. We have participated in two large-scale projects, sponsored by the Secretaries of State of California and Ohio, whose respective goals were to perform the security testing of the electronic voting systems used in those two states. The testing process identified major flaws in all the systems analyzed, and resulted in substantial changes in the voting procedures of both states. In this paper, we describe the testing methodology that we used in testing two real-world electronic voting systems, the findings of our analysis, and the lessons we learned.

This paper discusses the importance of keeping practitioners in mind when determining what research to pursue and when making design and implementation decisions as part of a research program. The author discussed how his 30 plus years of security research have been driven by the desire to provide products, tools, and techniques that are useful for practitioners. He also discussed his view of what new security challenges the future has in store for us.

Intrusion detection systems are distributed applications that analyze the events in a networked system to identify malicious behavior. The analysis is performed using a number of attack models (or signatures) that are matched against a specific event stream. Intrusion detection systems may operate in heterogeneous environments, analyzing different types of event streams. Currently, intrusion detection systems and the corresponding attack modeling languages are developed following an ad hoc approach to match the characteristics of specific target environments. As the number of systems that have to be protected increases, this approach results in increased development effort. To overcome this limitation, we developed a framework, called STAT, that supports the development of new intrusion detection functionality in a modular fashion. The STAT framework can be extended following a well-defined process to implement intrusion detection systems tailored to specific environments, platforms, and event streams. The STAT framework is novel in the fact that the extension process also includes the extension of the attack modeling language. The resulting intrusion detection systems represent a software family whose members share common attack modeling features and the ability to reconfigure their behavior dynamically. The STAT framework allows an Intrusion Detection Administrator to express high-level configuration requirements that are mapped automatically to a detailed deployment and/or reconfiguration plan. This approach supports automation of the administrator tasks and better assurance of the effectiveness and consistency of the deployed sensing infrastructure.

Intrusion detection systems monitor computer networks looking for evidence of malicious actions. Networks are complex systems, and a comprehensive intrusion detection solution has to be able to manage event streams with different content,speed, level of abstraction, and accessibility. Therefore, it is necessary to distribute intrusion detection sensors across multiple protected networks, manage their configuration as the security posture of the networks changes, and process the results of their analysis so that a high-level picture of the security state of the network can be provided to the administrators. This paper presents Hi-DRA, a network surveillance, analysis, and response system for high-speed WANs. The system provides a framework for the modular development of intrusion detection sensors in heterogeneous, high-speed environments. In addition, the system provides an infrastructure that supports the dynamic configuration of the sensors and the collection and interpretation of their results. The system, as a whole,is able to provide fine-grained monitoring across WANs and, at the same time,is able to correlate the results of the analysis of the different sensors into a high-level expressive description of security violations.

Mobile ad hoc network routing protocols are highly susceptible to subversion. Previous research in securing these protocols has typically used techniques based on encryption and redundant transmission. These techniques prevent a range of attacks against routing protocols but are expensive to deploy on energy-constrained wireless devices. Experience in securing wired networks has demonstrated that, in addition to intrusion prevention techniques, it is useful to deploy intrusion detection techniques as a second line of defense. In this paper, we discuss some of the threats to wireless ad hoc networks, and, specifically, some attacks against the AODV routing protocol. We also present a tool aimed at real-time detection of these attacks. The tool monitors network packets to detect local and distributed attacks within its radio range. Experiments show that the tool provides effective intrusion detection functionality while using only a limited amount of resources.

Alert correlation is a process that analyzes the alerts produced by one or more intrusion detection systems and provides a more succinct and high-level view of occurring or attempted intrusions. Even though the correlation process is often presented as a single step, the analysis is actually carried out by a number of components, each of which has a specific goal. Unfortunately, most approaches to correlation concentrate on just a few components of the process, providing formalisms and techniques that address only specific correlation issues. This paper presents a general correlation model that includes a comprehensive set of components and a framework based on this model. A tool using the framework has been applied to a number of well-known intrusion detection data sets to identify how each component contributes to the overall goals of correlation. The results of these experiments show that the correlation components are effective in achieving alert reduction and abstraction. They also show that the effectiveness of a component depends heavily on the nature of the data set analyzed.

Signature-based intrusion detection systems use a set of attack descriptions to analyze event streams, looking for evidence of malicious behavior. If the signatures are expressed in a well-defined language, it is possible to analyze the attack signatures and automatically generate events or series of events that conform to the attack descriptions. This approach has been used in tools whose goal is to force intrusion detection systems to generate a large number of detection alerts. The resulting "alert storm" is used to desensitize intrusion detection system administrators and hide attacks in the event stream. We apply a similar technique to perform testing of intrusion detection systems. Signatures from one intrusion detection system are used as input to an event stream generator that produces randomized synthetic events that match the input signatures. The resulting event stream is then fed to a number of different intrusion detection systems and the results are analyzed. This paper presents the general testing approach and describes the first prototype of a tool, called Mucus, that automatically generates network traffic using the signatures of the Snort network-based intrusion detection system. The paper describes preliminary cross-testing experiments with both an open-source and a commercial tool and reports the results. An evasion attack that was discovered as a result of analyzing the test results is also presented.

Web servers are ubiquitous, remotely accessible, and often misconfigured. In addition, custom Web-based applications may introduce vulnerabilities that are overlooked even by the most security-conscious server administrators. Consequently, Web servers are a popular target for hackers. To mitigate the security exposure associated with Web servers, intrusion detection systems are deployed to analyze and screen incoming requests. The goal is to perform early detection of malicious activity and possibly prevent more serious damage to the protected site. Even though intrusion detection is critical for the security of Web servers, the intrusion detection systems available today only perform very simple analyses and are often vulnerable to simple evasion techniques. In addition, most systems do not provide sophisticated attack languages that allow a system administrator to specify custom, complex attack scenarios to be detected. We present WebSTAT, an intrusion detection system that analyzes Web requests looking for evidence of malicious behavior. The system is novel in several ways. First of all, it provides a sophisticated language to describe multistep attacks in terms of states and transitions. In addition, the modular nature of the system supports the integrated analysis of network traffic sent to the server host, operating system-level audit data produced by the server host, and the access logs produced by the Web server. By correlating different streams of events, it is possible to achieve more effective detection of Web-based attacks.

As more business activities are being automated and an increasing number of computers are being used to store sensitive information, the need for secure computer systems becomes more apparent. This need is even more apparent as systems and applications are being distributed and accessed via an insecure network, such as the Internet. The Internet itself has become critical for governments, companies, financial institutions, and millions of everyday users. Networks of computers support a multitude of activities whose loss would all but cripple these organizations. As a consequence, cybersecurity issues have become national security issues. Protecting the Internet is a difficult task. Cybersecurity can be obtained only through systematic development; it can not be achieved through haphazard seat-of-the-pants methods. Applying software engineering techniques to the problem is a step in the right direction. However, software engineers need to be aware of the risks and security issues associated with the design, development, and deployment of network-based software. This paper introduces some known threats to cybersecurity, categorizes the threats, and analyzes protection mechanisms and techniques for countering the threats. Approaches to prevent, detect, and respond to cyber attacks are also discussed.

Intrusion detection systems are distributed applications that analyze the events in a networked system to identify malicious behavior. The analysis is performed using a number of attack models (or signatures) that are matched against a specific event stream. Intrusion detection systems may operate in heterogeneous environments, analyzing different types of event streams. Currently, intrusion detection systems and the corresponding attack modeling languages are developed following an ad hoc approach to match the characteristics of specific target environments. As the number of systems that have to be protected increases, this approach results in increased development effort. To overcome this limitation, we developed a framework, called STAT, that supports the development of new intrusion detection functionality in a modular fashion. The STAT framework can be extended following a well-defined process to implement intrusion detection systems tailored to specific environments, platforms, and event streams. The STAT framework is novel in the fact that the extension process also includes the extension of the attack modeling language. The resulting intrusion detection systems represent a software family whose members share common attack modeling features and the ability to reconfigure their behavior dynamically.

Secure computer systems use both mandatory and discretionary access controls to restrict the flow of information through legitimate communication channels such as files, shared memory and process signals. Unfortunately, in practice one finds that computer systems are built such that users are not limited to communicating only through the intended communication channels. As a result, a well-founded concern of security-conscious system designers is the potential exploitation of system storage locations and timing facilities to provide unforeseen communication channels to users. These illegitimate channels are known as covert storage and timing channels. Prior to the presentation of this paper twenty years ago the covert channel analysis that took place was mostly ad hoc. Methods for discovering and dealing with these channels were mostly informal, and the formal methods were restricted to a particular specification language. This paper presents a methodology for discovering storage and timing channels that can be used through all phases of the software life cycle to increase confidence that all channels have been identified. In the original paper the methodology was presented and applied to an example system having three different descriptions: English, formal specification, and high order language implementation. In this paper only the English requirements are considered. However the paper also presents how the methodology has evolved and the influence it had on other work.

Security analysis should take advantage of a reliable knowledge base that contains semantically-rich information about a protected network. This knowledge is provided by network mapping tools. These tools rely on models to represent the entities of interest, and they leverage off network discovery techniques to populate the model structure with the data that is pertinent to a specific target network. Unfortunately, existing tools rely on incomplete data models. Networks are complex systems and most approaches oversimplify their target models in an effort to limit the problem space. In addition, the techniques used to populate the models are limited in scope and are difficult to extend. This paper presents NetMap, a security tool for network modeling, discovery, and analysis. NetMap relies on a comprehensive network model that is not limited to a specific network level; it integrates network information throughout the layers. The model contains information about topology, infrastructure, and deployed services. In addition, the relationships among different entities in different layers of the model are made explicit. The modeled information is managed by using a suite of composable network tools that can determine various aspects of network configurations through scanning techniques and heuristics. Tools in the suite are responsible for a single, well-defined task.

As networks become faster there is an emerging need for security, analysis techniques that can keep up with the increased network throughput. Existing network-based intrusion detection sensors can barely, keep up with bandwidths of a few hundred Mbps. Analysis tools that can deal with higher throughput are unable to maintain state between different steps of an attack or they are limited to the analysis of packet headers. We propose a partitioning approach to network security, analysis that supports in-depth, stateful intrusion detection on high-speed links. The approach is centered around a slicing mechanism that divides the overall network traffic into subsets of manageable size. The traffic partitioning is done so that a single slice contains all the evidence necessary to detect a specific attack, making sensor-to-sensor interactions unnecessary. This paper describes the approach and presents a first experimental evaluation of its effectiveness.

STATL is an extensible state/transition-based attack description language designed to support intrusion detection. The language allows one to describe computer penetrations as sequences of actions that an attacker performs to compromise a computer system. A STATL description of an attack scenario c an be used by an intrusion detection system to analyze a stream of events and detect possible ongoing intrusions. Since intrusion detection is performed in different domains (i.e., the network or the hosts) and in different operating environments (e.g., Linux, Solaris, or Windows NT), it is useful to have an extensible language that can be easily tailored to different target environments. STATL defines domain-independent features of attack scenarios and provides constructs for extending the language to describe attacks in particular domains and environments. The STATL language has been successfully used in describing both network-based and host-based attacks, and it has been tailored to very different environments, e.g., Sun Microsystems' Solaris and Microsoft's Windows NT. An implementation of the runtime support for the STATL language has been developed and a toolset of intrusion detection systems based on STATL has been implemented. The toolset was used in a recent intrusion detection evaluation effort, delivering very favorable results. This paper presents the details of the STATL syntax and its semantics. Real examples from both the host and network-based extensions of the language are also presented.

The World Wide Web is playing a major role in reducing business costs and in providing convenience to users. Digital libraries capitalize on this technology to distribute documents that are stored in their servers. Online banks capitalize on this technology to reduce their operating costs and to offer 24 hour services to their clients. These two services are examples of services that require a high degree of security. Therefore, they require a higher level of protection than the existing technologies commonly used in the World Wide Web. An approach that can be used to protect Internet transactions, called Safe Areas of Computation, was described in (dos Santos and Kemmerer, 1999). This paper describes the access control lists used by the Safe Areas of Computation approach, the operations on these access control lists supported by the approach, and how the access control lists can be customized for implementing many different security policies. This paper also describes example policies that can be used to protect digital libraries and online bank services. The paper uses the bank services as an example of how the generic security policies supported by the SAC approach can be composed.

ASTRAL is a high-level formal specification language for real-time systems. It has structuring mechanisms that allow one to build modularized specifications of complex real-time systems with layering. Based upon the ASTRAL symbolic model checler reported in [13], three approximation techniques to speed-up the model checking process for use in debugging a specification are presented. The techniques are random walk, partial image and dynamic environment generation. Ten mutation tests on a railroad crossing benchmark are used to compare the performance of the techniques applied separately and in combination. The test results are presented and analyzed.

This paper presents three sets of classification schemes for processes, properties, and transitions that can be used to assist in the analysis of real-time systems. These classification schemes are discussed in the context of ASTRAL, which is a formal specification language for real-time systems. Eight testbed systems were specified in ASTRAL, and their proofs were performed to determine proof patterns that occur most often. The specifications were then examined in an attempt to derive specific characteristics that could be used to statically identify each pattern within a specification. Once the classifications were obtained, they were then used to provide systematic guidance for analyzing real-time systems by directing the prover to the proof techniques most applicable to each proof pattern. This paper presents the set of classification schemes that were developed and discusses how they can be used to assist the proof process.

Currently the computer systems and software used by the average user offer virtually no security. Because of this, many attacks, both simulated and real, have been described by the security community and have appeared in the popular press. The paper presents an approach to increase the level of security provided to users when interacting with otherwise unsafe applications and computing systems. The general approach, called Safe Areas of Computation (SAC), uses trusted devices, such as smart cards, to provide an area of secure processing and storage. The paper describes preliminary results of using the Safe Areas of Computation approach to protect specific browsing applications. The intent is for protected browsers to be used to interact with institutions that have requirements for high security, such as financial institutions that enable users to perform sensitive operations for electronic commerce or online banking.

Article Using the ASTRAL model checker to analyze mobile IP Share on Authors: Zhe Dang Reliable Software Group, Computer Science Department, University of California, Santa Barbara, CA Reliable Software Group, Computer Science Department, University of California, Santa Barbara, CAView Profile , Richard A. Kemmerer Reliable Software Group, Computer Science Department, University of California, Santa Barbara, CA Reliable Software Group, Computer Science Department, University of California, Santa Barbara, CAView Profile Authors Info & Claims ICSE '99: Proceedings of the 21st international conference on Software engineeringMay 1999 Pages 132–141https://doi.org/10.1145/302405.302459Online:16 May 1999Publication History 19citation272DownloadsMetricsTotal Citations19Total Downloads272Last 12 Months2Last 6 weeks0 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 SiteGet Access

Network-based attacks are becoming more common and sophisticated. For this reason, intrusion detection systems are now shifting their focus from the hosts and their operating systems to the network itself. Network-based intrusion detection is challen

Network-based attacks have become common and sophisticated. For this reason, intrusion detection systems are now shifting their focus from the hosts and their operating systems to the network itself. Network-based intrusion detection is challenging because network auditing produces large amounts of data, and different events related to a single intrusion may be visible in different places on the network. This paper presents NetSTAT, a new approach to network intrusion detection. By using a formal model of both the network and the attacks, NetSTAT is able to determine which network events have to be monitored and where they can be monitored.

No abstract available.

A real time computer system is a system that must perform its functions within specified time bounds. These systems are generally characterized by complex interactions with the environment in which they operate and strict time constraints whose violation may have catastrophic consequences. The need for these software systems to be highly reliable is evident. One way to achieve this reliability is through formal development. Although research in the area of real time systems has been quite active and a number of experimental environments supporting formal specifications have been developed, the search for adequate notations and tools is still ongoing. In order to get designers to use formal methods to develop real time systems it is necessary to provide them with an integrated set of tools for writing and analyzing their specifications. The ASTRAL Software Development Environment (SDE), which is an integrated set of tools based on the ASTRAL formal framework, is intended to meet this need. The tools that make up the support environment are a syntax directed editor, a specification processor, a verification condition generator, a mechanical theorem prover, and a browser kit. The paper discusses the goals for ASTRAL, why they were important, and how they were met. It also gives an overview of the ASTRAL Software Development Environment.

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A real-time system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the rationale of ASTRAL's design. ASTRAL's specification style is illustrated by discussing a telephony example. Composability of one or more ASTRAL system specifications is also discussed by the introduction of a composition section, which provides the needed information to combine two or more ASTRAL system specifications.

The covert channel analysis (CCA) approach presented in the paper leverages off of the subsystem architecture of the DG/UX kernel. The kernel is structured so that each of the elements of the system state is under the control of a single subsystem. That is, these elements can only be referenced or modified by functions of the controlling subsystem; thus, each subsystem can be thought of as an abstract object. In order to make the covert channel analysis task for the Trusted DG/UX kernel more manageable and, in particular, to deal with the Ratings Maintenance Program (RAMP), a modular approach that takes advantage of the subsystem architecture is used. The CCA approach used for analyzing DG/UX is to first perform an SRM analysis for each of the subsystems that contain an exported function directly invoked from one of the system calls. These subsystems are called "peer subsystems". The information from the SRMs for all of the peer subsystems is then used to build the kernel-wide SRM.

No abstract available.

The paper presents a new approach to representing and detecting computer penetrations in real time. The approach, called state transition analysis, models penetrations as a series of state changes that lead from an initial secure state to a target compromised state. State transition diagrams, the graphical representation of penetrations, identify precisely the requirements for and the compromise of a penetration and present only the critical events that must occur for the successful completion of the penetration. State transition diagrams are written to correspond to the states of an actual computer system, and these diagrams form the basis of a rule based expert system for detecting penetrations, called the state transition analysis tool (STAT). The design and implementation of a Unix specific prototype of this expert system, called USTAT, is also presented. This prototype provides a further illustration of the overall design and functionality of this intrusion detection approach. Lastly, STAT is compared to the functionality of comparable intrusion detection tools.>

This paper introduces Aslantest, a symbolic execution tool for the formal specification language Aslan. Aslan is a state-based specification language built on first-order predicate calculus with equality. Aslantest animates Aslan specifications and enables users to interactively run specific test cases or symbolically execute the specification. Testing the formal specifications early in the software life cycle allows one to assure a reliable system that also provides the desired functionality.

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL specifications. ASTRAL is provided with structuring mechanisms that allow one to build modularized specifications of complex systems with layering. In this paper, further details of the ASTRAL environment components and the critical requirements components, which were not fully developed in previous papers, are presented. Formal proofs in ASTRAL can be divided into two categories: interlevel proofs and intralevel proofs. The former deal with proving that the specification of level i+1 is consistent with the specification of level i, and the latter deal with proving that the specification of level i is consistent and satisfies the stated critical requirements. This paper concentrates on intralevel proofs.>

ASTRAL is a formal specification language for realtime systems. It is intended to support formal software development, and therefore has been formally defined. In ASTRAL a realtime system is modeled by a collection of state machine specifications and a single global specification.

A new approach to representing computer penetrations is introduced called penetration state transition analysis. This approach models penetrations as a series of state transitions described in terms of signature actions and state descriptions. State transition diagrams are written to correspond to the states of an actual computer system, and these diagrams form the basis of a rule-based expert system for detecting penetrations, referred to as STAT.>

A technique for detecting covert storage channels using a tree structure called a covert flow tree (CFT) is introduced. By traversing the paths of a CFT a comprehensive list of scenarios that potentially support covert communication via particular resource attributes can be automatically constructed. CFTs graphically illustrate the process through which information regarding the state of one attribute is relayed to another attribute, and how in turn that information is relayed to a listening process. Algorithms for automating the construction of CFT and potential covert channel operation sequences are presented. Two example systems are analyzed and their results are compared to two other analysis techniques performed on identical systems. The CFT approach not only identified all covert storage channels found by the other techniques, but discovered a channel not detected by the other techniques.>

The authors introduce a technique for detecting covert storage channels using a tree structure called a covert flow tree (CFT). CFTs are used to perform systematic searches for operation sequences that allow information to be relayed through attributes and eventually detected by a listening process. When traversed, the paths of a CFT yield a comprehensive list of operation sequences which support communication via a particular resource attribute. These operation sequences are then analyzed and either discharged as benign or determined to be covert communication channels. Algorithms for automating the construction of CFTs and potential covert channel operation sequences are presented. To illustrate this technique, two example systems are analyzed and their results compared to two currently accepted analysis techniques performed on identical systems. This comparison shows that the CFT approach not only identified all covert storage channels found by the other analysis techniques, but discovered a channel not detected by the other techniques.>

An approach to analyzing encryption protocols using machine-aided formal verification techniques is presented. The properties that the protocol should preserve are expressed as state invariants, and the theorems that must be proved to guarantee that the cryptographic facility satisfies the invariants are automatically generated by the verification system. A formal specification of an example system is presented, and several weaknesses that were revealed by attempting to verify and test the specification formally are discussed.>

This paper presents an approach to analyzing Encryption protocols using machine aided formal verification techniques. The desirable properties that a protocol is to preserve are expressed as state invariants and the theorems that need to be proved to guarantee that the cryptographic facility satisfies the invariants are automatically generated by the verification system. A formal specification of an example system is presented, and a weakness that was revealed by testing the formal specification is discussed.

This paper examines the application of two covert channel analysis techniques to a high level design for a real system, the Honeywell Secure Ada® Target (SAT). The techniques used were a version of the noninterference model of multilevel security due to Goguen and Meseguer and the shared resource matrix method of Kemmerer. Both techniques were applied to the Gypsy Abstract Model of the SAT. The paper discusses the application of the techniques and the nature of the covert channels discovered. The relative strengths and weaknesses of the two methods are discussed and criteria for an ideal covert channel tool are developed.

This paper examines the application of two covert channel analysis techniques to a high level design for a real system the Honeywell Secure Ada Target (SAT). The techniques used were a version of the non-interference model of multilevel security due to Goguen and Meseguer and the shared resource matrix method of Kemmerer. Both techniques were applied to the Gypsy abstract model of the SAT. The paper discusses the application of the techniques and the nature of the covert channels discovered. The relative strengths and weaknesses of the two methods are discussed and criteria for an ideal covert channel tool are developed.

RT-ASLAN, a formal language for specifying real-time systems, is an extension of the ASLAN specification language for sequential systems. Some of the features of the ASLAN language, such as constructs for writing procedural semantics in a nonprocedural logical language, are highlighted. The RT-ASLAN language supports specification of parallel real-time processes through arbitrary levels of abstraction; processes do not have to be specified to the same level of detail. Communicating processes use an interface process as an abstract data type representing shared information. From RT-ASLAN specifications, performance correctness conjectures are generated. These conjectures are logic statements whose proof guarantees that the specification meets critical time bounds. A detailed example as well as a discussion of the advantages and disadvantages of formal specification and verification are included.

Abstract UNISEX is a UNIX‐based symbolic executor for Pascal. The UNISEX system provides an environment for both testing and formally verifying Pascal programs. The system supports a large subset of Pascal, runs on UNIX and provides the user with a variety of debugging features to help in the difficult task of program validation. This paper contains a brief introduction to symbolic execution, followed by an overview of the features of UNISEX, a discussion of the UNISEX Pascal language, and some of the implementation details for the UNISEX system. Finally, some of the problems encountered when designing and implementing the system are discussed as well as future directions.

Formal specification and verification techniques are now apused to increase the reliability of software systems. However, these proaches sometimes result in specifying systems that cannot be realized or that are not usable. This paper demonstrates why it is necessary to test specifications early in the software life cycle to guarantee a system that meets its critical requirements and that also provides the desired functionality. Definitions to provide the framework for classifying the validity of a functional requirement with respect to a formal specification tion are also introduced. Finally, the design of two tools for testing formal specifications is discussed.

The SDC Secure Release Terminal SRT) project provides a useful view of the process involved in constructing software whose code is intended to be formally verified to satisfy desired security properties. The purpose of the SRT is to move appropriately classified data from a processing environment at one security level to a processing environment at another level in machine readable form. This paper discusses the design process for the SRT which was carried out using the SDC Formal Development Methodology (FDM). the SRT project is the first application of the FDM code level verification capabilities. However, since the code level verification has not yet been performed this paper concentrates on the design problems inherent in targeting a system for code level verification.

Recognizing and dealing with storage and timing channels when performing the security analysis of a computer system is an elusive task.Methods for discovering and dealing with these channels have mostly been informal, and formal methods have been restricted to a particular specification language.A methodology for discovering storage and timing channels that can be used through all phases of the software life cycle to increase confidence that all channels have been identified is presented.The methodology is presented and applied to an example system having three different descriptions: English, formal specification, and high-order language implementation.

Recognizing and dealing with storage and timing channels when performing the security analysis of a computer system is an elusive task. Methods of discovering and dealing with these channels for the most part have been ad hoc, and those that are not are restricted to a particular specification language. This paper outlines a practical methodology for discovering storage and timing channels that can be used through all phases of the software life cycle to increase the assurance that all channels have been identified. The methodology is presented and its application to three different descriptions (English, formal specification, and high order language implementation) are discussed.

Data Secure Unix, a kernel structured operating system, was constructed as part of an ongoing effort at UCLA to develop procedures by which operating systems can be produced and shown secure. Program verification methods were extensively applied as a constructive means of demonstrating security enforcement.