Catálogo de publicaciones - libros

There is a growing need for systems whose survivability in a specified use and/or attack environment can be assured with confidence. Many techniques have been proposed to validate individual components (e.g., formal methods) or a system as a whole (e.g., red teaming). However, no single technique can provide the breadth of evidence needed to validate a system with respect to high-level survivability requirements. To accomplish this, we propose an integrated validation procedure (IVP) that begins with the formulation of a specific survivability requirement R and determines whether a system is valid with respect to R. The IVP employs a top-down approach that methodically breaks the task of validation into manageable tasks, and for each task, applies techniques best suited to its accomplishment. These efforts can be largely independent, and the results, which complement and supplement each other, are integrated to provide a convincing assurance argument. We then illustrate the IVP by applying it to an intrusion-tolerant information system being developed by the U.S. Department of Defense. In addition to validating the system against high-level survivability requirements, we demonstrate the use of model-based validation techniques, as a part of the overall validation procedure, to guide the system’s design by exploring different configurations and evaluating tradeoffs.

The development of dependable distributed systems needs to be based on a proper foundation. This foundation is generally given in form of a system and failure model. The system model defines the semantics of basic services like process and message services of a distributed system. More advanced system services will be based on these basic services. The failure model specifies the likely failures of the basic services, i.e., these are the failures that the advanced system services need to cope with.

The objective of the system and failure model is the following. As long as the assumptions of the failure and system model are valid, a system has to guarantee its specification. However, if these assumptions are violated during run-time, the system specification might be violated. The probability that a dependable system violates its specification must be negligible. Therefore, the probability of the occurrence of failures which are not specified by the failure model must also be negligible.

Nowadays information technology (IT) is increasingly determining growth in the world of automation. After it changed hierarchies, structures and flows in the entire office world, it now covers all the sectors from the process and manufacturing industries to logistics and building automation. The communications capability of devices and continuous, transparent information routes are indispensable components of future-oriented automation concepts.

In a previous work we validated an ODBMS component injecting errors in the application’s interface. The aim was to observe the robustness of the component when the application that interacted with it failed. In this work we tackle the injection of errors directly into the interfaces among the target component’s classes. As the component under test has several classes, we use stratified sampling to reduce the amount of injections without losing the ability to detect faults. Strata are defined based on a complexity metric, Weighted Methods in a Class – WMC. Experiments show that this metric alone is not sufficient to select strata for testing purposes.

This paper presents a methodology for the automated detection of buffer overflow vulnerabilities in executable software. Buffer overflow exploitation has been used by hackers to breach security or simply to crash computer systems. The mere presence inside the software code of a vulnerability that allows for buffer overflow exploitations presents a serious risk. So far, all methodologies devised to mitigate this problem assume source code availability or prior knowledge on vulnerable functions. Our methodology removes this dependency and allows the analysis of executable code without any knowledge about its internal structure. This independence is fundamental for relevant scenarios such as COTS selection during system integration (for which source code is usually not available), and the definition of attackloads for dependability benchmarking.

In this paper we present NekoStat, an extension of the Neko tool. Neko is a Java framework and a communication platform that permits rapid prototyping of distributed applications; it provides tools to organize the applications using a layered architecture, with the network(s) at the bottom of the architecture. Neko is also a communication platform that allows sending and receiving of generic Java objects. Distributed systems realized within the Neko framework can be exercised both on real networks and on simulated ones, without changes in the application code. We constructed an extension to plain Neko, called NekoStat; it permits attainment of quantitative evaluations of distributed systems. In the paper we describe this extension; we motivate the development of NekoStat, we describe the design and finally we illustrate its usage through a case study, which highlights the usefulness of NekoStat.

In the civil aviation certification the software has an unlike treatment due to its peculiarities and also for being a relatively new item. There is no specific software certification requirement in the FAR – FAR 33.28 is the only section that mentions the word . The FAA recognizes the considerations presented in RTCA/DO-178B as an acceptable means for approval of software used in airborne systems for civil aviation. The CTA/IFI/CAvC, responsible for the type certification in Brazil, has been applying RTCA/DO-178B since it was issued. The purpose of this paper is to present the experience of CTA in applying DO-178B, focusing on those technical issues that were source of controversy among certification authorities and industries. This paper is relevant at present time as RTCA and EUROCAE have recently organized a intending to issue DO-178C by the end of 2008.

The design, implementation and testing of the exceptional activity of a software system are complex tasks that usually do not receive the necessary attention from existing development methodologies. This work presents a systematic way to deal with exception handling, from the requirement specification phase to the implementation and testing phases, in component-based software development. Testing activities are performed since the early stages of development, promoting an increase in the quality of the produced system. Our solution refines the Methodology for the Definition of Exception Behavior, MDCE, in the architectural design, implementation, and testing phases. Moreover, the proposed method was adapted to the UML Components process.

Assuring the correctness of fault-tolerant distributed systems can be an overwhelming task. Besides dealing with complex problems of distributed systems, it is also necessary to design the system in such a way that a well-defined failure behaviour, or the masking of failure components, is presented by the system when components fail. To help reasoning about such systems, the use of formal methods becomes desirable. In previous work we introduced a graphical formal specification language, called Object-Based Graph Grammars (OBGG), for modelling asynchronous distributed systems. We also defined a method for automatically inserting classical fault behaviours into OBGG models. The obtained models could be analysed using simulation. In this paper a new method for automatically inserting fault behaviours into OBGG models, which is suitable for using verification as the analysis method, is proposed. Moreover, we show how to formally verify OBGG models in the presence of such faults. A two phase commit protocol is used to illustrate the contributions.

A growing number of safety-critical systems is controlled by computer systems. Currently these systems are often built from scratch. The Zerberus System assists the developer in the design and implementation process. Main features of the Zerberus System are generality, dependability, real-time predictability, the ability to be certified and cost-efficiency.

The main concept of the Zerberus System is the platform independent specification of the functional model by the developer. The functional model specifies the functional elements (tasks), the relation between these elements, the interaction of the system with the environment and the temporal constraints. On the base of the functional model the Zerberus System automatically generates the fault-tolerance mechanisms. Thus the task of the developer is restricted to the implementation of the application-dependent code.

In this paper we present one major part of the Zerberus System: the Zerberus Language that is used to specify the functional model of the control applications.