Flaky tests are tests that can non-deterministically pass or fail, even in the absence of code changes. Despite being a source of false alarms, flaky tests often remain in test suites once they are detected, as they also may be relied upon to detect true failures. Hence, a key open problem in flaky test research is: How to quickly determine if a test failed due to flakiness, or if it detected a bug? The state-of-the-practice is for developers to re-run failing tests: if a test fails and then passes, it is flaky by definition; if the test persistently fails, it is likely a true failure. However, this approach can be both ineffective and inefficient. An alternate approach that developers may already use for triaging test failures is failure de-duplication, which matches newly discovered test failures to previously witnessed flaky and true failures. However, because flaky test failure symptoms might resemble those of true failures, there is a risk of miss classifying a true test failure as a flaky failure to be ignored. Using a dataset of 498 flaky tests from 22 open-source Java projects, we collect a large dataset of 230,439 failure messages (both flaky and not), allowing us to empirically investigate the efficacy of failure de-duplication. We find that for some projects, this approach is extremely effective (with 100% specificity), while for other projects, the approach is entirely ineffective. By analyzing the characteristics of these flaky and non-flaky failures, we provide useful guidance on how developers should rely on this approach.

Over the past decade, hundreds of fuzzers have been published in top-tier security and software engineering conferences. Fuzzers are used to automatically test programs, ideally creating high-coverage input corpora and finding bugs. Modern “greybox” fuzzers evolve a corpus of inputs by applying mutations to inputs and then executing those new inputs while collecting coverage. New inputs that are “interesting” (e.g. reveal new coverage) are saved to the corpus. Given their non-deterministic nature, the impact of each design decision on the fuzzer’s performance can be difficult to predict. Some design decisions (e.g., ” Should the fuzzer perform deterministic mutations of inputs? ”) are exposed to end-users as configuration flags, but others (e.g., ” What kinds of random mutations to apply to inputs?”) are typically baked into the fuzzer code itself. This paper describes our over 12.5-CPU-year evaluation of the set of mutation operators employed by the popular AFL++ fuzzer, including the havoc phase, splicing, and, exploring the impact of adjusting some of those unexposed configurations. In this experience paper, we propose a methodology for determining different fuzzers’ behavioral diversity with respect to branch coverage and bug detection using rigorous statistical methods. Our key finding is that, across a range of targets, disabling certain mutation operators (some of which were previously “baked-in” to the fuzzer) resulted in inputs that cover different lines of code and reveal different bugs. A surprising result is disabling certain mutators leads to more diverse coverage and allows the fuzzer to find more bugs faster. We call for researchers to investigate seemingly simple design decisions in fuzzers more thoroughly and encourage fuzzer developers to expose more configuration parameters pertaining to these design decisions to end users.

Mutation testing offers concrete test goals (mutants) and a rigorous test efficacy criterion, but it is expensive due to vast numbers of mutants, many of which are neither useful nor actionable. Prior work has focused on selecting representative and sufficient mutant subsets, measuring whether a test set that is mutation-adequate for the subset is equally adequate for the entire set. However, no known industrial application of mutation testing uses or even computes mutation adequacy, instead focusing on iteratively presenting very few mutants as concrete test goals for developers to write tests.

Fuzz testing (fuzzing) allows developers to detect bugs and vulnerabilities in code by automatically generating defect-revealing inputs. Most fuzzers operate by generating inputs for applications and mutating the bytes of those inputs, guiding the fuzzing process with branch coverage feedback via instrumentation. Whitebox guidance (e.g., taint tracking or concolic execution) is sometimes integrated with coverage-guided fuzzing to help cover tricky-to-reach branches that are guarded by complex conditions (so-called "magic values"). This integration typically takes the form of a targeted input mutation, e.g., placing particular byte values at a specific offset of some input in order to cover a branch. However, these dynamic analysis techniques are not perfect in practice, which can result in the loss of important relationships between input bytes and branch predicates, thus reducing the effective power of the technique. We introduce a new, surprisingly simple, but effective technique, global hinting, which allows the fuzzer to insert these interesting bytes not only at a targeted position, but in any position of any input. We implemented this idea in Java, creating Confetti, which uses both targeted and global hints for fuzzing. In an empirical comparison with two baseline approaches, a state-of-the-art greybox Java fuzzer and a version of Confetti without global hinting, we found that Confetti covers more branches and finds 15 previously unreported bugs, including 9 that neither baseline could find. By conducting a post-mortem analysis of Confetti's execution, we determined that global hinting was at least as effective at revealing new coverage as traditional, targeted hinting.

The research community has long recognized a complex interrelationship between fault detection, test adequacy criteria, and test set size. However, there is substantial confusion about whether and how to experimentally control for test set size when assessing how well an adequacy criterion is correlated with fault detection and when comparing test adequacy criteria. Resolving the confusion, this paper makes the following contributions: (1) A review of contradictory analyses of the relationships between fault detection, test adequacy criteria, and test set size. Specifically, this paper addresses the supposed contradiction of prior work and explains why test set size is neither a confounding variable, as previously suggested, nor an independent variable that should be experimentally manipulated. (2) An explication and discussion of the experimental designs of prior work, together with a discussion of conceptual and statistical problems, as well as specific guidelines for future work. (3) A methodology for comparing test adequacy criteria on an equal basis, which accounts for test set size without directly manipulating it through unrealistic stratification. (4) An empirical evaluation that compares the effectiveness of coverage-based testing, mutation-based testing, and random testing. Additionally, this paper proposes probabilistic coupling, a methodology for assessing the representativeness of a set of test goals for a given fault and for approximating the fault-detection probability of adequate test sets.

Existing mutation techniques produce vast numbers of equivalent, trivial, and redundant mutants. Selective mutation strategies aim to reduce the inherent redundancy of full mutation analysis to obtain most of its benefit for a fraction of the cost. Unfortunately, recent research has shown that there is no fixed selective mutation strategy that is effective across a broad range of programs; the utility (i.e., usefulness) of a mutant produced by a given mutation operator varies greatly across programs.

The Self-Paced Learning Increases Retention and Capacity (SPARC) project is responding to the well-documented surge in CS enrollment by creating a self-paced learning environment that blends online learning, automated assessment, collaborative practice, and peer-supported learning. SPARC delivers educational material online, encourages students to practice programming in groups, frees them to learn material at their own pace, and allows them to demonstrate proficiency at any time. This model contrasts with traditional course offerings, which impose a single schedule of due dates and exams for all students. SPARC allows students to complete courses faster or slower at a pace tailored to the individual, thereby allowing universities to teach more students with the same or fewer resources. This paper describes the goals and elements of the SPARC model as applied to CS1. We present results so far and discuss the future of the project.

Various forms of selective mutation testing have long been accepted as valid approximations to full mutation testing. This paper presents counterevidence to traditional selective mutation. The recent development of dominator mutants and minimal mutation analysis lets us analyze selective mutation without the noise introduced by the redundancy inherent in traditional mutation. We then exhaustively evaluate all small sets of mutation operators for the Proteum mutation system and determine dominator mutation scores and required work for each of these sets on an empirical test bed. The results show that all possible selective mutation approaches have poor dominator mutation scores on at least some of these programs. This suggests that to achieve high performance with respect to full mutation analysis, selective approaches will have to become more sophisticated, possibly by choosing mutants based on the specifics of the artifact under test, that is, specialized selective mutation.

Mutation analysis generates tests that distinguish variations, or mutants, of an artifact from the original. Mutation analysis is widely considered to be a powerful approach to testing, and hence is often used to evaluate other test criteria in terms of mutation score, which is the fraction of mutants that are killed by a test set. But mutation analysis is also known to provide large numbers of redundant mutants, and these mutants can inflate the mutation score. While mutation approaches broadly characterized as reduced mutation try to eliminate redundant mutants, the literature lacks a theoretical result that articulates just how many mutants are needed in any given situation. Hence, there is, at present, no way to characterize the contribution of, for example, a particular approach to reduced mutation with respect to any theoretical minimal set of mutants. This paper's contribution is to provide such a theoretical foundation for mutant set minimization. The central theoretical result of the paper shows how to minimize efficiently mutant sets with respect to a set of test cases. We evaluate our method with a widely-used benchmark.

As a test criterion, mutation analysis is known for yielding very effective tests. It is also known for creating many test requirements, each of which is represented by a "mutant" that must be "killed." In recent years, researchers have found that these test requirements have a lot of duplication, in that many test requirements yield the same tests. Put another way, hundreds of mutants can usually be killed by only a few dozen tests. If we could reduce this duplication without reducing mutation's effectiveness, mutation testing could become more cost-effective. One avenue of this research has been to use only one type of mutant, the statement deletion mutation operator. Researchers have found that statement deletion mutation has relatively few mutants, but yields tests that are almost as effective as using all mutants, with the significant benefit that fewer equivalent mutants are generated. This paper extends this idea by asking a simple question: if deleting statements is a cost-effective way to design tests, will deleting other program elements also be effective? This paper presents results from mutation operators that delete variables, operators, and constants, finding that indeed, this is an efficient and effective approach.

Test driven development (TDD) is the practice of writing unit tests before writing the source. TDD practitioners typically start with example-based unit tests to verify an understanding of the software's intended functionality and to drive software design decisions. Hence, the typical role of test cases in TDD leans more towards specifying and documenting expected behavior, and less towards detecting faults. Conversely, traditional criteria-based test coverage ignores functionality in favor of tests that thoroughly exercise the software. This paper examines whether it is possible to combine both approaches. Specifically, can additional criteria based tests improve the quality of TDD test suites without disrupting the TDD development process? This paper presents the results of an observational study that generated additional criteria-based tests as part of a TDD exercise. The criterion was mutation analysis and the additional tests were designed to kill mutants not killed by the TDD tests. The additional unit tests found several software faults and other deficiencies in the software. Subsequent interviews with the programmers indicated that they welcomed the additional tests, and that the additional tests did not inhibit their productivity.

There are two driving questions in software test automation: first, which tests to select out of a potentially infinite set of inputs, and second, whether the system under test exhibits an error when executing the chosen tests. Model-based testing (MBT) offers an answer to both of these questions. Models serve as a rich source of tests, and researchers have devised a wide range of techniques for selecting representative sets of tests. At the same time, the models encode the expected behaviour of the systems under test, and so the model answers the question of the expected output as well. The idea of MBT dates back to the 1970s, when people started using finite state machines for testing. Since then, an active international community has grown around this topic. Today, there are several workshops with years-long traditions (Workshop on Advances in Model-based Testing (A-MOST), Workshop on Model-based Testing (MBT), Workshop on Model-based Testing in Practice (MOTIP), Workshop on Model-Driven Engineering, Verification, and Validation (MoDeVVa), Workshop on Model-Based Verification and Validation (MVV), Model-Based Testing User Conference (MBTUC), etc.), papers on MBT appear at all major software engineering conferences and journals, there have been three Dagstuhl seminars dedicated to the topic, and several books on MBT have been published. Furthermore, reports of industrial success and companies that earn their living by providing MBT tools are clear indications that the topic has matured from a pure research topic into a successfully applied industrial technology. We received 29 submissions for this special issue. Reviewing followed the same process as for regular papers. Each paper was reviewed by at least three reviewers, and after a rigorous selection process requiring a total of 25 revisions and 100 reviews, nine papers remain for publication. These papers are spread across three special issues of STVR; this issue includes the first three papers, covering the foundations of MBT and offering an industrial perspective. The first paper, ‘A Taxonomy of Model-Based Testing Approaches’ by Mark Utting, Alexander Pretschner and Bruno Legeard, aims to organize a taxonomy describing the technologies and characteristics of the different MBT approaches that have been proposed over the years. This paper is based on a technical report from 2006, which is already very well known in the community and has 136 citations at the time of this writing, showing that it does an excellent job at capturing the essence of MBT. The second paper, ‘Obstacles and Opportunities in Deploying Model-Based GUI Testing of Mobile Software: A Survey’ by Marek Janicki, Mika Katara and Tuula Pääkkönen, investigates possible obstacles and opportunities towards wider deployment of MBT in industry. The paper is based on a survey conducted among engineers and managers involved in testing of mobile software that work in companies domiciled in Finland. The survey is based on a methodology called the TEMA toolset, which is introduced to the participants to give them an idea how MBT could work. Besides an evaluation of the TEMA toolset, the survey helps to identify the challenges in test automation, obstacles to MBT adoption, and identify metrics and reports that can convince managers to adopt MBT. The third paper, ‘Applying Formal Methods to PCEP: An Industrial Case Study from Modelling to Test Generation’ by Iksoon Hwang, Ana Cavalli, Mounir Lallali and Dominique Verchere, offers insights based on an industrial case study. In their study, the authors apply formal methods to model, verify and validate the Path Computation Element Communication Protocol. The protocol is modelled using the IF language, and test cases are produced using the automated test generation tool TestGen-IF. This article not only demonstrates the benefits of automated testing but also describes the authors’ experiences in identifying modelling errors—an aspect that should not be overlooked when applying MBT. All the contributions presented in this and the two upcoming special issues on MBT reveal the broad and dynamic MBT research community. This was possible through the combined efforts of all authors and reviewers, and we wish to thank them all for their time and energy. The following persons were the reviewers: Bernhard Aichernig, Andrea Arcuri, Phillips Aydal, Benoit Baudry, Fevzi Belli, Robert Binder, Paul Black, Gregor von Bochmann, Kirill Bogdanov, Sergiy Boroday, Fabrice Bouquet, Lydie du Bousquet, Harald Brandl, Mario Bravetti, Lionel Briand, José Campos, Ana Cavalli, Charles Colbourn, Mirko Conrad, Steve Counsell, Frederic Dadeau, Hyunsook Do, Juan Dueñas, Khaled El-Fakih, Phyllis Frankl, Angelo Gargantini, Sudipto Ghosh, Wolfgang Grieskamp, Mats Grindal, Florian Gross, Roland Groz, Qiang Guo, Atul Gupta, Mark Harman, Alan Hartman, Robert Hierons, Daniel Hoffman, Antti Huima, Florentin Ipate, Guy-Vincent Jourdan, AbdulSalam Kalaji, Gregory Kapfhammer, Mika Katara, Raimund Kirner, Pieter Koopman, Bogdan Korel, Willibald Krenn, Richard Kuhn, Victor Kuliamin, Raluca Lefticaru, Bruno Legeard, Johan Lilius, Michael Linschulte, Atif Memon, Mercedes Merayo, Marius Mikucionis, Tim Miller, Ralf Mitsching, Laurent Mounier, Henry Muccini, Brian Nielsen, Manuel Nunez, Ana Paiva, Amit Paradkar, Ioannis Parissis, Fabio Paternò, Patrizio Pelliccione, Alexandre Petrenko, Andrea Polini, Alexander Pretschner, Tuula Pääkkönen, Debra Richardson, Ismael Rodríguez, Gregg Rothermel, Vlad Rusu, Manoranjan Satpathy, Ina Schieferdecker, Rudolf Schlatte, Holger Schlingloff, Julien Schmaltz, José Silva, Adenilso Simao, Paul Strooper, Harold Thimbleby, Nikolai Tillmann, Paolo Tonella, Yves Le Traon, Guilherme Travassos, Jan Tretmans, Tugkan Tuglular, Hasan Ural, M. Uyar, Neil Walkinshaw, Martin Weiglhofer, Carsten Weise, Stephan Weissleder, Lee White, Marco Winckler, Jim Woodcock, Fatiha Zaïdi, and Tewfik Ziadi.

The need for better software continues to rise, as do expectations. This, in turn, puts more emphasis on finding problems before software is released. Industry is responding by testing more, but many test engineers in industry lack a practical, yet theoretically sound, understanding of testing. Software engineering educators must respond by teaching students to test better. An essential testing skill is designing tests, and an efficient way to design high quality tests is to use an engineering approach: test criteria. To achieve the maximum benefit, criteria should be used during unit (developer) testing, as well as integration and system testing. This paper presents an in-depth teaching experience report on how we successfully teach criteria-based test design using abstraction and publicly accessible web applications. Our teaching materials are freely available online or upon request.

Abstract Logic criteria demand inputs that guarantee detection of certain faults. One such criterion, MUMCUT, is composed of three criteria, where each constituent criterion ensures the detection of specific faults. In practice, the criteria may overlap in terms of faults detected, leading to redundant tests, but due to the fact that infeasible requirements do not result in tests, all the constituent criteria are needed. The key insight of this paper is that analysis of the feasibility of the constituent criteria can reduce test set size without sacrificing fault detection for specific faults. This paper introduces a new logic criterion, Minimal‐MUMCUT, and shows how it can apply to minimal DNF, minimal CNF, and general form Boolean expressions. With Minimal‐MUMCUT, a determination is made of which constituent criteria are feasible, and hence necessary, at the level of individual literals and terms. An empirical study found that Minimal‐MUMCUT reduces the test set size, without sacrificing fault detection, regardless of the predicate format. Copyright © 2011 John Wiley & Sons, Ltd.

Some software testing logic coverage criteria demand inputs that guarantee detection of a large set of fault types. One powerful such criterion, MUMCUT, is composed of three criteria, where each constituent criterion ensures the detection of specific fault types. In practice, the criteria may overlap in terms of fault types detected, thereby leading to numerous redundant tests, but due to the unfortunate fact that infeasible test requirements don't result in tests, all the constituent criteria are needed. The key insight of this paper is that analysis of the feasibility of the constituent criteria can be used to reduce test set size without sacrificing fault detection. In other words, expensive criteria can be reserved for use only when they are actually necessary. This paper introduces a new logic criterion, Minimal-MUMCUT, based on this insight. Given a predicate in minimal DNF, a determination is made of which constituent criteria are feasible at the level of individual literals and terms. This in turn determines which criteria are necessary, again at the level of individual literals and terms. This paper presents an empirical study using predicates in avionics software. The study found that Minimal-MUMCUT reduces test set size -- without sacrificing fault detection -- to as little as a few percent of the test set size needed if feasibility is not considered.

Mutation testing is a technique for generating high quality test data. However, logic mutation testing is currently inefficient for three reasons. One, the same mutant is generated more than once. Two, mutants are generated that are guaranteed to be killed by a test that kills some other generated mutant. Three, mutants that when killed are guaranteed to kill many other mutants are not generated as valuable mutation operators are missing. This paper improves logic mutation testing by 1) extending a logic fault hierarchy to include existing logic mutation operators, 2) introducing new logic mutation operators based on existing faults in the hierarchy, 3) introducing new logic mutation operators having no corresponding faults in the hierarchy and extending the hierarchy to include them, and 4) addressing the precise effects of equivalent mutants on the fault hierarchy. An empirical study using minimal DNF predicates in avionics software showed that a new logic mutation testing approach generates fewer mutants, detects more faults, and outperforms an existing logic criterion.

Abstract About a decade after the initial proposal to use model checkers for the generation of test cases we take a look at the results in this field of research. Model checkers are formal verification tools, capable of providing counterexamples to violated properties. Normally, these counterexamples are meant to guide an analyst when searching for the root cause of a property violation. They are, however, also very useful as test cases. Many different approaches have been presented, many problems have been solved, yet many issues remain. This survey paper reviews the state of the art in testing with model checkers. Copyright © 2008 John Wiley & Sons, Ltd.

Abstract Many software logic test coverage criteria have emerged over the past several years; however, they are scattered throughout the literature. The goal of this paper is to describe the various logic tests and explain their rationale in a centralized location in order to aid software testers in their decisions about which to implement. Each logic test is examined in terms of its minimum and maximum test sizes, subsumption relationship to other logic tests, and its fault detection capability. It is shown that although semantic tests generally have a smaller test size, syntactic tests are better in terms of fault detection capability. Furthermore, it is shown that the syntactic tests subsume their semantic counterparts. Two new software faults are introduced to Kuhn's fault hierarchy, namely the term insertion fault and the term negation fault, and the fault detection capability of the logic tests with respect to these faults is examined. A new software testing criterion called multiple unique true point/near false point (MUTP/NFP) is also presented, with a description of its benefits and limitations. Specifically, a detailed comparison of the MUTP/NFP criterion and the CUTPNFP/MNFP/MUTP criterion is given. Copyright © 2008 John Wiley & Sons, Ltd.

Can-follow concurrency control permits a transactionto read (write) an item write-locked (read-locked) by anothertransaction with almost no delays. By combining the merits of2PL and 2V2PL, this approach mitigates the lock contention notonly between update and read-only transactions, but also betweenupdate and update transactions.

The typical means by which an attacker breaks into a network is through a chain of exploits, where each exploit in the chain lays the groundwork for subsequent exploits. Such a chain is called an attack path, and the set of all possible attack paths form an attack graph. Researchers have proposed a variety of methods to generate attack graphs. In this paper, we provide a novel alternative approach to network vulnerability analysis by utilizing a penetration tester's perspective of maximal level of penetration possible on a host. Our approach has the following benefits: it provides a more intuitive model in which an analyst can work, and its algorithmic complexity is polynomial in the size of the network, and so has the potential of scaling well to practical networks. The drawback is that we track only "good" attack paths, as opposed to all possible attack paths. Hence, an analyst may make suboptimal choices when repairing the network. Since attack graphs grow exponentially with the size of the network, we argue that suboptimal solutions are an unavoidable cost of scalability, and hence practical utility. A working prototype tool has been implemented to demonstrate the practicality of our approach.

A large number of coverage criteria to generate tests from logical expressions have been proposed. Although there have been large variations in the terminology, the articulation of the criteria and the original source of the expressions, many of these criteria are fundamentally the same. The most commonly known and widely used criterion is that of modified condition decision coverage (MCDC), but some articulations of MCDC have had some ambiguities. This has led to confusion on the part of testers, students, and tool developers on how best to implement these test criteria. This paper presents a complete comprehensive set of criteria that incorporate all the existing criteria, and eliminates the ambiguities by introducing precise definitions of the various possibilities.

Abstract Although the majority of software testing in industry is conducted at the system level, most formal research has focused on the unit level. As a result, most system‐level testing techniques are only described informally. This paper presents formal testing criteria for system level testing that are based on formal specifications of the software. Software testing can only be formalized and quantified when a solid basis for test generation can be defined. Formal specifications represent a significant opportunity for testing because they precisely describe what functions the software is supposed to provide in a form that can be automatically manipulated. This paper presents general criteria for generating test inputs from state‐based specifications. The criteria include techniques for generating tests at several levels of abstraction for specifications (transition predicates, transitions, pairs of transitions and sequences of transitions). These techniques provide coverage criteria that are based on the specifications and are made up of several parts, including test prefixes that contain inputs necessary to put the software into the appropriate state for the test values. The test generation process includes several steps for transforming specifications to tests. These criteria have been applied to a case study to compare their ability to detect seeded faults. Copyright © 2003 John Wiley & Sons, Ltd.

Even well administered networks are vulnerable to attack. Recent work in network security has focused on the fact that combinations of exploits are the typical means by which an attacker breaks into a network. Researchers have proposed a variety of graph-based algorithms to generate attack trees (or graphs). Either structure represents all possible sequences of exploits, where any given exploit can take advantage of the penetration achieved by prior exploits in its chain, and the final exploit in the chain achieves the attacker's goal. The most recent approach in this line of work uses a modified version of the model checker NuSMV as a powerful inference engine for chaining together network exploits, compactly representing attack graphs, and identifying minimal sets of exploits. However, it is also well known that model checkers suffer from scalability problems, and there is good reason to doubt whether a model checker can handle directly a realistic set of exploits for even a modest-sized network. In this paper, we revisit the idea of attack graphs themselves, and argue that they represent more information explicitly than is necessary for the analyst. Instead, we propose a more compact and scalable representation. Although we show that it is possible to produce attack trees from our representation, we argue that more useful information can be produced, for larger networks, while bypassing the attack tree step. Our approach relies on an explicit assumption of monotonicity, which, in essence, states that the precondition of a given exploit is never invalidated by the successful application of another exploit. In other words, the attacker never needs to backtrack. The assumption reduces the complexity of the analysis problem from exponential to polynomial, thereby bringing even very large networks within reach of analysis

Preventive measures sometimes fail to deflect malicious attacks. We adopt an information warfare perspective, which assumes success by the attacker in achieving partial, but not complete, damage. In particular, we work in the database context and consider recovery from malicious but committed transactions. Traditional recovery mechanisms do not address this problem, except for complete rollbacks, which undo the work of benign transactions as well as malicious ones, and compensating transactions, whose utility depends on application semantics. Recovery is complicated by the presence of benign transactions that depend, directly or indirectly, on the malicious transactions. We present algorithms to restore only the damaged part of the database. We identify the information that needs to be maintained for such algorithms. The initial algorithms repair damage to quiescent databases; subsequent algorithms increase availability by allowing new transactions to execute concurrently with the repair process. Also, via a study of benchmarks, we show practical examples of how offline analysis can efficiently provide the necessary data to repair the damage of malicious transactions.

In addition to providing a sound basis for analysis, formal methods can support other development activities; in our case the target is specification-based testing at the system level. We use the formal method of model checking to either generate new test sets or analyze existing test sets with respect to safety properties expressed in a temporal logic. We consider two types of tests: failing tests, in which a system must reject (fail) a specific dangerous action, and passing tests, in which a system must accept (pass) a safe action in a context that also includes a plausible dangerous action. We formalize our notion of dangerous actions with a mutation model for model checking specifications, and we develop coverage criteria to assess test sets. The coverage criteria are based on the logic operators from the Computation Tree Logic (CTL) and encompass the idea of scenarios where a dangerous action is either inevitable (A) or possible (E) as of the next state (X) or at some point in the future (F). We demonstrate the feasibility of our approach with an example.

This paper compares three specification-based testing criteria using Mathur and Wong's PROBSUBSUMES measure. The three criteria are specification-mutation coverage, full predicate coverage, and transition-pair coverage. A novel aspect of the work is that each criterion is encoded in a model checker, and the model checker is used first to generate test sets for each criterion and then to evaluate test sets against alternate criteria. Significantly, the use of the model checker for generation of test sets eliminates human bias from this phase of the experiment. The strengths and weaknesses of the criteria are discussed.

Even well administered networks are vulnerable to attacks due to the security ramifications of offering a variety of combined services. That is, services that are secure when offered in isolation nonetheless provide an attacker with a vulnerability to exploit when offered simultaneously. Many current tools address vulnerabilities in the context of a single host. We address vulnerabilities due to the configuration of various hosts in a network. In a different line of research, formal methods are often useful for generating test cases, and model checkers are particularly adept at this task due to their ability to generate counterexamples. We address the network vulnerabilities problem with test cases, which amount to attack scenarios, generated by a model checker. We encode the vulnerabilities in a state machine description suitable for a model checker and then assert that an attacker cannot acquire a given privilege on a given host. The model checker either offers assurance that the assertion is true on the actual network or provides a counterexample detailing each step of a successful attack.

Update anywhere-anytime-anyway transactional replication has unstable behavior as the workload scales up. To reduce this problem, a two-tier replication algorithm is proposed in (Gray et al., 1996) that allows mobile applications to propose tentative transactions that are later applied to a master copy. However it can suffer from heavy reprocessing overhead in many circumstances. We present the method of merging histories instead of reprocessing to reduce the overhead of two-tier replication. The basic idea is when a mobile node connects to the base nodes merging the tentative history into the base history so that substantial work of tentative transactions could be saved. As a result, a set of undesirable transactions (denoted B) have to be backed out to resolve the conflicts between the two histories. Desirable transactions that are affected directly or indirectly, by the transactions in B complicate the process of backing out B. We present a family of novel rewriting algorithms for the purpose of backing out B. By incorporating transaction semantics, our rewriting methods are strictly better at saving desirable tentative transactions than the traditional reads-from transitive-closure based approach. In most cases our rewriting methods are better at saving desirable tentative transactions than an approach which is based only on commutativity.

We apply a model checker to the problem of test generation using a new application of mutation analysis. We define syntactic operators, each of which produces a slight variation on a given model. The operators define a form of mutation analysis at the level of the model checker specification. A model checker generates countersamples which distinguish the variations from the original specification. The countersamples can easily be turned into complete test cases, that is, with inputs and expected results. We define two classes of operators: those that produce test cases from which a correct implementation must differ, and those that produce test cases with which it must agree. There are substantial advantages to combining a model checker with mutation analysis. First, test case generation is automatic; each countersample is a complete test case. Second, in sharp contrast to program-based mutation analysis, equivalent mutant identification is also automatic. We apply our method to an example specification and evaluate the resulting test sets with coverage metrics on a Java implementation.

Multilevel transactions have been proposed for multilevel secure databases; in contrast to most proposals, such transactions allow users to read and write across multiple security levels. The security requirement that no high level operation influence a low level operation often conflicts with the atomicity requirement of the standard transaction processing model. In particular, others have shown that no concurrency control algorithm based on the standard transaction processing model can guarantee both atomicity and security. This conflict motivates us to propose an alternative semantic-based transaction processing model for multilevel transactions. Our model uses the semantics of the application to analyze an application and reason about its behavior. Our notion of correctness is based on semantic correctness instead of serializability as in the standard transaction processing model. Semantic correctness ensures that database consistency is maintained, transactions output consistent data, and all partially executed transactions complete. We show how an example application can be analyzed to assure semantic correctness and how this analysis can be automated. We also propose a simple timestamp-based multiversion concurrency control algorithm for transaction processing on a kernelized architecture. The advantages of our model over the standard transaction processing model are that atomicity can be assessed, and for some applications ensured via off line analysis, more concurrency is achieved, lesser synchronization between security levels is required, and a larger class of multilevel transactions can be processed.

Software engineering is a rapidly changing discipline, and will continue to be so for the foreseeable future. This pace of change brings both problems and opportunities to universities that teach software engineering. Engineers ore no longer satisfied with one or two initial university education experiences, but by necessity are becoming lifetime learners, with frequent trips back to educational providers. This recurring education is needed to update engineers' knowledge with new ideas and concepts, and to update engineers' skills. In this paper, we take the position that universities can and should respond to this situation with a new model for graduate software engineering education, which we call professional currency certificates. These courses should offer the depth of knowledge and university academic credit that traditional academic courses offer, but with the convenience and practical nature of corporate training courses. This hybrid model results in a new kind of course that more closely meets the needs of lifetime learners.

We consider the problem of surviving information warfare attacks on databases. We adopt a fault tolerance approach to the different phases of an attack. To maintain precise information about the attack, we mark data to reflect the severity of detected damage as well as the degree to which the damaged data has been repaired. In the case of partially repaired data, integrity constraints might be violated, but data is nonetheless available to support mission objectives. We define a notion of consistency suitable for databases in which some information is known to be damaged, and other information is known to be only partially repaired. We present a protocol for normal transactions with respect to the damage markings and show that consistency preserving normal transactions maintain database consistency in the presence of damage. We present an algorithm for taking consistent snapshots of databases under attack. The snapshot algorithm has the virtue of not interfering with countermeasure transactions.

In some database applications the traditional approach of seerializability, in which transactions appear to execute atomically and in isolation on a consistent database state, fails to satisfy performance requirements. Although many researchers have investigated the process of decomposing transactions into steps to increase concurrency, such research typically focuses on providing algorithms necessary to implement a decomposition supplied by the database application developer and pays relatively little attention to what constitutess a desirable decomposition or how the developer should obtain one. We focus onthe decomposition itself. A decomposition generates proof obligations whose descharge ensures desirable properties with respect to the original collection of transactions. We introduce the notion of semantic histories to formulate and prove the necessary properties, and the notion of successor sets to describe efficiently the correct interleavings of steps. The successor set constraints use information about conflicts between steps so as to take full advantage of conflict serializability at the level of steps. We propose a mechanism based on two-phase locking to generate correct stepwise serializable histories.

Ensuring atomicity is a major outstanding problem with present methods of handling multilevel transactions. The chief difficulty is that a high section of a transaction may be unable to complete due to violations of the integrity constraints, and a rollback of sections can be exploited to implement a covert channel. We define a notion of semantic atomicity which guarantees that either all or none of the sections of a transaction are present in any history. The notion of correct executions in our model is based on semantic correctness-that is, maintenance of integrity constraints-rather than serializability. We give a method whereby the application developer can statically analyze the set of transactions in the application and determine if the set ensures semantic atomicity and other desirable properties.

Formal demonstration of equivalence or nonequivalence of different security models helps identify the fundamental constructs and principles in such models. In this paper, we demonstrate the nonequivalence of two monotonic access control models that differ only in the creation operation for new subj ects and/or objects; in particular, we show that single-parent creation is less expressive than multi-parent creation. The nature of the proof indicates that this result will apply to any monotonic access control model. The nonequivalence proof is carried out on an abstract access control model, following which the results are interpreted in standard formulations. In particular, we apply the results to demonstrate nonequivalence of the Schematic Protection Model (SPM) and the Extended Schematic Protection Model (ESPM). We also show how the results apply to the typed access matrix model (TAM), which is an extension of the well known access matrix model formalized by Harrison, Ruzzo and Ullman (HRU). The results in this paper offer theoretical justification for regarding single-parent and multi-parent creation as fundamentally different operations in a monotonic context. The paper also demonstrates that in nonmonotonic models, multi-parent creation can be reduced to single-parent creation, thereby neutralizing the difference in expressive power.

We consider communication structures for event ordering algorithms in distributed environments where information flows only in one direction. Example applications are multilevel security and hierarchically decomposed databases. Although the most general one directional communication structure is a partial order, partial orders do not enjoy the property of being consistently ordered, a formalization of the notion that local ordering decisions are ensured to be globally consistent. Our main result is that the crown free property is necessary and sufficient for a communication structure to be consistently ordered. We discuss the computational complexity of detecting crowns and sketch typical applications.

We offer a concurrency conirol algorithm for replicated, secure, multilevel databases. We compare the algorithm with a multiversion approach and with the typical full-replication approach. In the full-replication approach, each security level maintains a container that holds a complete copy of data at lower security levels. In the approach described here, access to data at lower security levels is through shared, read-only snapshots, where a constant number of snapshots at each level – two, as it turns out – is sufficient. We derive necessary properties for snapshots, give a switching algorithm to assign read-downs to snapshots, specify a snapshot creation algorithm, demonstrate that the approach is free of indirect channels and starvation, and prove one-copy serializability on execution histories. In contrast to some comparable algorithms, our algorithm is correct for any security structure that is a partial order.

The partitioned synchronization rule is a technique for proving the correctness of concurrency control algorithms. Prior work has shown the applicability of the partitioned synchronization rule to hierarchically decomposed databases whose structure is restricted to semitrees. The principal contribution of the paper is a demonstration that the partitioned synchronization rule also applies to more general structures than semitrees, specifically, to any planar extendible partial order, a partial order which when extended with a least and a greatest element still remains planar. To demonstrate utility, the paper presents two applications of the partitioned synchronization rule. The first application shows correctness of a component based timestamp generation algorithm suitable for implementing a timestamp ordering concurrency control algorithm. The second application shows correctness of a snapshot algorithm for concurrency control in a replicated multilevel secure database; we choose this application to highlight that hierarchically decomposed databases and multilevel secure databases are structurally similar. In both cases, the correctness proofs via the partitioned synchronization rule are substantially simpler than corresponding direct proofs.>

A common database need is to obtain a global-read, which is a consistent read of an entire database. To avoid terminating normal system activity, and thus improve availability, we propose an on-the-fly algorithm that reads database entities incrementally and allows normal transactions to proceed concurrently. The algorithm assigns each entity a color based on whether the entity has been globally read, and a shade based on how normal transactions have accessed the entity. Serializability of execution histories is ensured by requiring normal transactions to pass both a color test and a shade test before being allowed to commit. Our algorithm improves on a color-only-based scheme from the literature; the color-only scheme does not guarantee serializability.>

We propose an efficient multiversion algorithm for servicing read requests in secure multilevel databases. Rather than keep an arbitrary number of versions of a datum, as standard multiversion algorithms do, the algorithm presented here maintains only a small fixed number of versions—up to three—for a modified datum. Each version corresponds to the state of the datum at the end of an externally defined version period. The algorithm avoids both covert channels and starvation of high transactions, and applies to security structures that are arbitrary partial orders. The algorithm also offers long-read transactions at any security level conflict-free access to a consistent, though slightly dated, view of any authorized portion of the database. We derive constraints sufficient to guarantee one-copy serializability of executions histories, and then exhibit an algorithm that satisfies these constraints.

We consider the propagation of authorizations in distributed database systems. If no constraints are imposed on the propagation of authorization changes, then the authorization states at different sites may evolve inconsistently. A standard solution is to suppress the distributed aspect and make all changes appear as if they had occurred in some serial order at a single site, perhaps via an atomic commit protocol. However, rigid insistence on consistency may result in authorization changes being needlessly delayed, a problem exacerbated in the context of site or communication failures. We propose an optimistic authorization propagation algorithm. We specify an authorization table and a set of operations for altering the authorization table. Each site maintains a log of authorization operations. We exploit the semantics of authorization operations to avoid relying on an undo-redo mechanism for processing out of order operations. Instead we give efficient, direct algorithms to scan the log and update the authorization table. Any inconsistencies in replicas of the authorization table are transient and are eliminated by further communication between sites. We discuss pruning the authorization log.

We analyze the safety question for the Non-Monotonic Transform (NMT) model, an access control model that encompasses a wide variety of practical access control mechanisms. In general, safety analysis, i.e. whether it is possible for a specified subject to obtain a given access right for a certain object, is computationally intractable, even for many monotonic models. We identify one-representable NMT schemes and argue that they have tractable safety analysis. Safety analysis of one-representable schemes considers exactly one representative of each type of subject in the initial state, and thus the complexity of safety analysis is independent of the total number of subjects in the system. We demonstrate by example that one-representable schemes admit applications of practical interest, and that safety analysis guides the construction of such schemes.>

Measurement of software reliability by life testing involves executing the software on large numbers of test cases and recording the results. The number of failures observed is used to bound the failure probability even if the number of failures observed is zero. Typical analyses assume that all failures that occur are observed, but, in practice, failures occur without being observed. In this paper, we examine the effect of imperfect error detection, i.e. the situation in which a failure of the software may not be observed. If a conventional analysis associated with life testing is used, the confidence in the bound on the failure probability is optimistic. Our results show that imperfect error detection does not necessarily limit the ability of life testing to bound the probability of failure to the very low values required in critical systems. However, we show that the confidence level associated with a bound on failure probability cannot necessarily be made as high as desired, unless very strong assumptions are made about the error detection mechanism. Such assumptions are unlikely to be met in practice, and so life testing is likely to be useful only for situations in which very high confidence levels are not required.>

Timestamps are considered for distributed environments in which information flow is restricted to one direction through a planar lattice imposed on a network. For applications in such networks, existing timestamping algorithms require extension and modification. For example, in secure environments, typical timestamps provide a potential signaling channel between incomparable levels. In hierarchical databases, typical timestamps cause peripheral sites to unnecessarily affect the behavior at main sites. Algorithms are presented by which a network node may generate and compare timestamps using timestamp components maintained at dominated nodes in the network. The comparison relation is shown to be acyclic for timestamps produced by the generation algorithm. We discuss ways to safely relax the requirement that the network be a lattice. By example, we show how to modify a simple nonplanar lattice so that the generation algorithm can be applied. Uses of the timestamp generation algorithm in the motivating applications are outlined.

Separation of duties is an important, real-world requirement that access control models should support. The transaction control expression (TCE) for specifying dynamic separation of duties was previously introduced. The implementation of TCEs in the typed access matrix model (TAM) is considered. It is shown that TAM requires extension for satisfactory handling of dynamic separation of duties. In particular, dynamic separation requires the capability to explicitly test for the absence of rights in cells of the access matrix. It is illustrated how TAM, extended to incorporate such tests, can implement TCEs. The impact of checks for absence of rights on safety analysis is discussed (i.e. the determination of whether or not a given subject can acquire a given right to a given object).>

Formal demonstration of equivalence or nonequivalence of different security models helps identify the fundamental constructs and principles in such models. The authors demonstrate the nonequivalence of two monotonic access control models that differ only in the creation operation for new subjects and/or objects; in particular, they show that single-parent creation is less expressive than multi-parent creation in monotonic models. The paper also demonstrates that in nonmonotonic models, multi-parent creation can be reduced to single-parent creation, thereby neutralizing the difference in expressive power. The nonequivalence proof is carried out on an abstract access control model, following which the results are interpreted in standard formulations. In particular, they apply the results to demonstrate nonequivalence of the schematic protection model (SPM) and the extended schematic protection model (ESPM). They also show how the results apply to the typed access matrix model (TAM).>

A concurrency control algorithm for replicated, secure, multilevel databases is presented. Multiversion and replicated databases can avoid starvation problems without introducing indirect channels by maintaining stable copies of old low-level data values for use by high-level transactions. The algorithm presented improves on two comparable techniques, a direct multiversion approach of T. F. Keefe and W. T. Tsai and the full replication scheme of S. Jajodia and B. Kogan (both in Proc. 1990 IEEE Symp. on Res. In Security & Privacy, May 1990). In the latter, each security level has a container that holds a copy of all lower-level data. It is shown that only a constant number of old copies (two, as it turns out) must be maintained. The correctness of the algorithm is argued, and it is demonstrated that the algorithm is free of indirect channels and starvation.>

Access control models provide a formalism and framework for specifying control over access to information and other resources in multi-user computer systems. Useful access control models must balance expressive power with the decidability and complex

Protection models provide a formalism for specifying control over access to information and other resources in a multi-user computer system. One such model, the extended schematic protection model (ESPM) has expressive power equivalent to the monotonic access matrix model of Harrison, Ruzzo, and Ullman (1976). Yet ESPM retains tractable safety analysis for many cases of practical interest. Thus ESPM is a very general model, and it is of interest whether ESPM can be implemented in a reasonable manner. The authors outline a distributed implementation for ESPM. The implementation is capability-based, with an architecture where servers act as mediators to all subject and object access. Capabilities are made nontransferable by burying the identity of subjects in them, and unforgeable by using a public key encryption algorithm. Timestamps and public keys are used as mechanisms for revocation.>

It is argued that the access matrix model of M.H. Harrison, W.L. Ruzzo and J.D. Ullman (HRU) (1976) has extremely weak safety properties; safety analysis is undecidable for most policies of practical interest. An alternate formulation of the HRU model is presented that gives strong safety properties. This alternative formulation is called the extended schematic protection model (ESPM). ESPM is derived from the schematic protection model (SPM) by extending the creation operation to allow multiple parents for a child, as opposed to the conventional create operation of SPM, which has a single parent for a child. It is shown that, despite its equivalence to HRU, ESPM, retains a tractable safety analysis for a large class of protection schemes that are of practical interest.>

Protection models provide a formalism for specifying control over access to information and other resources in a multi-user computer system. Useful protection models must balance expressive power with the complexity of safety analysis i.e. the determination of whether or not a given subject can ever acquire access to a given resource. The authors argue that, in terms of expressive power, a joint creation operation is a natural candidate for inclusion in an access control model, particularly in the context of integrity considerations. They extend the Schematic Protection Model (SPM) to allow for groups of subjects to jointly create other subjects and objects. They discuss the safety properties of ESPM. Despite the increase in expressive power, ESPM retains tractable safety analysis for many cases of practical interest.>

Data diversity is described, and the results of a pilot study are presented. The regions of the input space that cause failure for certain experimental programs are discussed, and data reexpression, the way in which alternate input data sets can be obtained, is examined. A description is given of the retry block which is the data-diverse equivalent of the recovery block, and a model of the retry block, together with some empirical results is presented. N-copy programming which is the data-diverse equivalent of N-version programming is considered, and a simple model and some empirical results are also given.>