Succinct Visual Evidence for Certifying
Mathematical Analysis of Software

1 Introduction

Software failures have caused serious accidents that resulted in death, injury, and large financial losses. Without intervention, the increasingly pervasive use of software may bring more frequent and more serious accidents. The National Academy of Sciences report on Software for Dependable Systems [12] points out that existing certification schemes that are intended to ensure the dependability of software have a mixed record; some are largely ineffective, and some are counterproductive. The National Academy Report [12] notes that conventional certification techniques based on conformance to development processes and testing cannot guarantee software compliance with critically important safety and security properties.

DO-178C [10] and UK Def Stan 00-56 [32] are well-known certification standards. Both standards require the submission of a reasoned justification as to why and how the verification and validation techniques achieve the certification goals. Safety arguments are typically communicated in existing safety cases through free text. For example, a safety case in UK Def Stan 00-56 is defined as: “ A structured argument, supported by a body of evidence that provides a compelling, comprehensible and valid case that a system is safe for a given application in a given operating environment.”

Unlike DO-178C, where testing evidence takes the front seat, UK Def Stan 00-56 gives precedence to analytical evidence. Nonetheless, in order to obtain credit for the use of mathematical analysis as the primary means for compliance, the mathematical methods should be accompanied with supporting evidence for reasoned justification. In practice, testing is the dominant technique for producing reasoned justification. All test cases are generated from the requirements. The quality of testing is judged against two coverage metrics: requirements coverage and structural coverage. While the first type of coverage determines which requirements were not tested, the latter determines how well the test cases exercised the code structure. The general approach that one must take in constructing an argument for replacing testing with another technology is to show how to argue that the evidence produced by the replacement technology is at least as convincing as the evidence produced by testing [17].

Security vulnerabilities can undermine the case made for dependability properties in software. The dependability properties must therefore account explicitly for security risks that might compromise its other aspects. It is also important to ensure that security certifications give meaningful assurance of resistance to attacks. Testing in general does not suffice for assuring software security, because even the largest test suites typically used do not exercise enough paths to provide evidence that the software is free from vulnerabilities. New security certification regimes are needed that can provide confidence that most attacks against certified products or systems will fail.

In this paper, we present a novel graphical notion of the certification evidence (CE) and its accompanied schema that mathematical analyses can produce and can be used for certification. For a practical adoption of our research, we have examined DO-178C [10] and UK Def Stan 00-56 [32] certification documents to arrive at a suitable notion of CE that can go along with prevalent practices in industry. We also present case studies from the Linux kernel and other software that illustrate how the novel CE schema is applicable in practice.

A summary of research contributions: (a) a novel certification evidence (CE) schema designed to clearly express the verification proof in a succinct visual form for the purpose of certification (Section 2), (b) Linux case studies to bring out the importance and the ease of use of the CE evidence (Section 4.1), and (c) a case study of a denial-of-service vulnerability in Bftpd software [4] to show how pitfalls in safety arguments can be avoided by using the CE schema (Section 4.2).

2 Certification Evidence Schema

This section describes a novel certification evidence (CE) schema designed to justify the verification proof in a succinct visual form to make it easy to comprehend and cross-check the proof. We shall use the memory leak (ML) problem as an example to concretely illustrate the different aspects of the general schema.

The ML verification requires a proof for each memory allocation instance. Thus, the CE schema must serve to provide the verification evidence for each instance.

2.1 Evidence Provided with the CE Schema

The CE schema is designed to provide the following evidence:

• Relevant Functions: The set of functions that are relevant in the verification proof. The set could have one or more functions. For example, it is just one function if a memory allocation in function f1 is followed by a memory deallocation in f1 itself, on each feasible control flow (CF) path following the allocation. However, it could be two functions f1 and f2 if there is a feasible CF path in f1 on which another function f2 deallocates the memory.
• Relations between Relevant Functions: The data and control relations between relevant functions. For example, the control and data relations can be respectively f1 calls f2 and f1 passes the pointer to the allocated memory to f2.
• Coverage of CF Paths: The evidence shows a grouping of all CF paths within each relevant function.The grouping is for the purpose of a concise proof. The number of CF paths grows exponentially with 2ⁿ paths with n non-nesting branch conditions. The paths where the same reasoning is applicable are put in one group. For example, the CF paths following a memory allocation in f1 may have three groups: (i) paths with deallocation, (ii) paths on which a pointer to the allocated memory is passed to f2, (iii) paths without deallocation on which the pointer is not passed to another function.
• Path Feasibility and Relevant Conditions: The evidence accounts for the path feasibility verification in order to avoid false positives. For example, feasibility must be checked for paths without deallocation on which the pointer is not passed to another function. It is not a memory leak if these paths are not feasible. The evidence includes the set of conditions relevant for checking the feasibility of a path.

2.2 A Graphical Notation for the CE Schema

We present a graphical notation as a succinct visual medium to communicate the certification evidence. We shall use the term macro evidence for the first two categories of evidence (relevant functions and relations between relevant functions) and the term micro evidence for the last two categories of evidence (coverage of CF paths and path feasibility).

The CE schema depicts the relevant functions as nodes and interactions between the functions as edges. Suppose the interaction is: function f passes a pointer to the allocated memory as a parameter to another function g. Then, the schema has an edge from f to g with label par to denote relevant parameter passing.

The CE schema is extensive enough to describe a variety of data and control flow interactions between functions. It incorporates all three modes of communicating data between functions: (i) passed as a parameter, (ii) passed as return value, and (iii) shared through a global variable. It incorporates all three modes for passing control from one function to another: (a) one function calls another function by name, (b) one function calls another function using a function pointer, and (c) two functions work asynchronously and so the control passes from one function to another because of context switching.

Unification of Macro and Micro Evidence: The micro evidence shows that the control flow paths within a function f are grouped into different groups for the purpose of verification. The macro evidence shows interactions of f with other functions for the purpose of verification. Consider the following scenario that calls for unification of macro and micro evidence. Start with function f that allocates memory. The control flow paths in function f fall into three groups: a group of control paths that include deallocation, a group of control paths that pass a pointer to the allocated memory to function g, and a third group of control paths that do not have either, i.e. they do not include deallocation and they do not communicate the pointer to allocated memory to any other function. We need to represent succinctly the grouping of paths (micro evidence) and the relevant passing of parameter (macro evidence).

Let us now discuss how the micro and macro evidence are unified to communicate the above scenario. As shown in Figure 1, the functions f and g are denoted by nodes. The three outgoing edges from f correspond to the three groups of control paths. An edge from f to g with label par denotes the relevant parameter passing along a group of paths. An edge from f to deallocation denotes the matching deallocation along a group of paths. An edge from f with label PFC denotes that a path feasibility check (PFC) is performed along a group of paths.

2.3 Evidence for a Real-World Example Using the CE Schema

We have chosen this example from the XINU operating system which is about 10,000 lines of code [8]. In XINU getbuf and freebuf are respectively the calls to allocate and deallocate memory. The memory in dgwrite is allocated by the getbuf call. We will use the CE schema to present evidence that every feasible CF path following this allocation in dgwrite has a corresponding freebuf call.

CE Evidence: As Figure 2 illustrates, the problem starts with memory allocation instance (getbuf call) in function dgwrite. The paths in dgwrite fall into two groups: paths with matching freebuf, and paths on which the pointer to the allocated memory is passed as a parameter to function udpsend. The parameter passing is shown by an edge from dgwrite to udpsend with the edge label par.

As per the CE evidence shown in Figure 2, the verification has taken the following steps:

1. Paths in udpsend fall into one group and the pointer to the allocated memory is passed as a parameter from udpsend to ipsend.
2. Paths in ipsend fall into one group and the pointer to the allocated memory is passed as a parameter from ipsend to route.
3. Paths in route fall into two groups. The pointer to the allocated memory is passed as a parameter from route to write along one group of paths and there is a matching freebuf along the other group of paths.
4. Paths in write fall into one group and the pointer to the allocated memory is passed as a parameter from write to ethwrite. write calls ethwrite using a function pointer. The function pointer call is denoted by the edge label fpc.
5. Paths in ethwrite fall into one group and the pointer to the allocated memory is passed as a parameter from ethwrite to ethwstrt.
6. Paths in ethwstrt fall into one group and the pointer to the allocated memory is assigned to the global variable dcmptr. The function ethinter reads that global variable.
7. Paths in ethinter fall into five groups. One group of paths have a matching freebuf. The other four groups of paths do not have a matching freebuf and the pointer to the allocated memory is not communicated to any other function. These four group of paths require path feasibility checks as donated by the edge label PFC.

Path Feasibility Check: We propose the use of the Projected Control Graph (PCG) [34] as a compact and easy-to-understand abstraction to capture micro evidence; it captures the relevant behaviors and relevant conditions for feasibility check. A control flow graph (CFG) can have many irrelevant conditions and a multitude of paths with identical relevant behavior for the purpose of verification, while the PCG has only one path per relevant behavior and captures only the relevant conditions.

The PCG for ethinter is shown in Figure 3(a); it shows six groups of paths. Two groups of paths have a matching freebuf (collapsed into one in Figure 2) and the other four groups of paths requiring feasibility checks are numbered 1 to 4 in Figure 3(a). The conditions relevant for checking path feasibility are captured by the PCG. An equivalent representation of the path feasibility conditions using a tabular notation is shown in Figure 3(b). The four groups of paths, all require feasibility checks but are still maintained as distinct paths because their corresponding relevant conditions are not the same and thus the feasibility checks are actually different.

Data and control relations between functions: This example brings out two out of the three data relations between functions: parameter passing and global variables. It also illustrates all three control relations between functions: a function is called by name, a function is called using a function pointer, and asynchronous control between two functions (the control is passed from ethwstrt to ethinter by context-switch; ethinter is an interrupt-driven function).

2.4 Applicability of the CE Schema

The CE schema is well-suited for verifying safety and security properties. Many safety and security properties are similar in terms of analysis and verification challenges they pose. A typical safety property can be stated as: verify that an event e₁(O) is followed by an event e₂(O) on every feasible execution path, where the two events are operations on the same object O (e.g., lock must be followed by unlock). A typical security property can be stated as: verify that an event e₁(O) is not followed by an event e₂(O) on every feasible execution path, where the two events are operations on the same object O. For example, a confidentiality property is: a sensitive source must not be followed by a malicious sink on any feasible execution path. We will refer to such safety and security properties as 2-event matching. Our case studies in Section 4 include the Lock-Unlock Pairing (LUP) and the Memory Leak (ML).

As a general application, the CE schema is useful for presenting evidence for verifying a property defined by a finite state machine (FSM): verify on every feasible CF path, the occurrence of events that follow the acceptability test defined by a FSM.

2.5 Strengths of CE Schema

The CE schema makes certification of mathematical analysis practical by focusing on evidence that the certifying authority can easily understand. The evidence focuses on what the mathematical analysis has achieved and not on how it works. Focusing on what is important to create evidence that is easy to understand. For example, to certify that a prime factorization algorithm is correct, one can give the prime factors it produces as the evidence. To understand the correctness of a prime factorization algorithm, you may have to be a number theorist. However, without knowing how they are produced, one can easily check the given prime factors are correct.

The CE schema provides a succint visual representation of evidence. It uses a structured graphical representation to present the evidence in visual form. Well-structured safety arguments are often given in text, however, there are problems experienced when text is the only medium for expressing complex arguments [23]. A graphical notation is desirable for safety arguments [23].

The CE schema succinctly reflects the aspects of software that have an important role in convincing that the mathematical verification is correct. It provides a correspondence between the mathematical proof and the software behavior at run-time. From the multitude of software artifacts and relationships, it distills only the elements that control the behaviors relevant for the certification goals. In doing so, it bridges the gap between the model for mathematical analysis and the actual software. This is particularly important if mathematical analyses are to be used for compliance, without the need to exercise the software at run-time.

The CE schema is well suited in constructing an argument for replacing testing with mathematical verification. Both standards, DO-178C [10] and UK Def Stan 00-56 [32], require the submission of a reasoned justification as to why and how the verification and validation techniques achieve the certification goals. In practice, testing is the dominant technique for producing reasoned justification. The quality of testing is judged against two coverage measures: requirements coverage and structural coverage. The CE schema includes evidence about coverage of all CF paths and their feasibility.

The CE schema is well-suited to include security considerations in the dependability case. Security vulnerabilities can undermine the case made for dependability properties in software. The dependability case must therefore account explicitly for security risks that might compromise its other aspects. It is also important to ensure that security certifications give meaningful assurance of resistance to attack. Testing in general does not suffice for assuring software security, because even the largest test suites do not exercise enough paths to provide evidence that the software is free from vulnerabilities. The CE schema focuses on the evidence that can show how the CF paths are covered.

The CE schema offers several other desirable attributes. We bring out some of these attributes through our case studies in Section 4. The CE schema produces evidence that can provide insights to improve mathematical analysis. A security or safety property may have thousands of instances that need to be verified. It would be too much burden on the certifying authority to go through so many instances one at a time. The CE schema enables categorization of instances based on the similarity of the evidence. The work for the certifying authority is much less if thousands of instances can be reduced to a small number categories so that certification can be based on the categories instead of individual instances. The CE schema is designed to look for exhaustive evidence, it helps in judging whether the evidence is complete and thus helps in avoiding pitfalls in making safety arguments.

2.6 Limitations of CE Schema

The CE schema currently does not encompass the evidence to support verification problems that can arise from faulty hardware-software co-design. For example, the CE schema does not include evidence to support time and space requirements of real-time embedded systems. These are important requirements for avionics, automotive, medical, and other safety-critical systems. The European Space Agency has set up the COMPASS project (Correctness, Modeling, and Performance of Aerospace Systems) [5]. Its goal is to develop a coherent and multidisciplinary approach towards developing systems at a systems engineering level. The COMPASS project has adopted the Architecture and Analysis Design Language (AADL) and its Error Model Annex [2] as the key formalism. Thus, a worthwhile exercise is to extend the CE schema to incorporate evidence based on AADL models.

3 Related Work

With software taking on an ever-greater role in modern systems, “correct code” requires more than just the developer’s claim [1]. Companies want to avoid expensive field support, product recalls, or legal actions due to software failures. Alongside, there are many myths about software qualification and certification [1].

Software certification calls for special considerations as discussed in numerous papers [11, 18–20, 22, 31]. It is about conformance of software artifacts to certain properties. For the purpose of conformance, Heck et al. [20] describe the following categories of properties: (a) consistency - do different (parts of) software artifacts conform to each other?, (b) functional - does input to the system produce the expected output?, (c) behavioral - does the system meet general safety properties like absence of deadlocks?, (d) quality - do the artifacts fulfill nonfunctional requirements in the areas of performance, security, and usability?, (e) compliance - do the artifacts conform to standards, guidelines, or legislation? While this categorization needs refinement, it is a good start.

Rushby observed in 1996 paper [15]: “Despite years of research, the overall impact of formal methods on mainstream software design has been disappointing. By contrast, formal methods are beginning to make real inroads in commercial hardware design.”. This situation continues to be a concern and numerous articles have been written on why formal methods are not used more widely [15, 24, 25, 30].

The new standard, DO-178C [10] has a supplement on formal methods, known as DO-333, which states the following: Formal methods might be used in a very selective manner to partially address a small set of objectives, or might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification. Overall, there is a growing interest in use of formal methods for software certification [12, 17, 21, 28].

Parnas observes [29]: “Software design is engineering. Engineers use mathematics routinely in much of their work. Software designers should do the same. Mathematical methods offered to the working software engineer are not very practical and are not much like the mathematics used by engineering.” In a landmark paper [13] on program verification and proofs in mathematics, De Millo, Lipton and Perlis (the first recipients of the Turing Award) argue that tools for program verification must provide evidence to support verification. With the growing need for software assurance for mission-critical systems, there is renewed interest in automated verification with evidence [9].

The ideas presented in this paper originate from our research on DARPA cybersecurity programs APAC [3] and STAC [7]. Our research on graphical techniques [14] to reason about complex software security problems led to the CE schema presented in this paper.

4 Case Studies

We present case studies from the Linux kernel and Bftpd software [4] to bring out the importance of CE evidence in a couple of different ways.

4.1 Linux Kernel Case Studies

The verification experiments are for: (a) Lock-Unlock Pairing (LUP) and (b) Memory Leak (ML). Both case studies include the verification of three Linux versions, altogether 37 million lines of code. We enabled all possible x86 build configurations via allmodconfig flag. The verification experiments are performed using the LDV [6] and the EV [27] model checkers.

The analyzed instances are categorized as: verified as safe, verified as unsafe and incomplete verification. LDV has potential bug as an additional category. LDV produces a counter example for an unsafe instance. LDV does not produce evidence to support its verification of safe instances. The traces it produces for incomplete instances are voluminous and difficult to understand.

The study shows the performance difference between LDV and EV model checkers. LDV does not report any sure bug. Interestingly, one Lock bug found by EV is actually an instance that is erroneously verified as safe by LDV. This bug is described in paper [26]. EV produces evidence for all instances including safe instances. The evidence for safe instances is critically important for certification.

Our initial speculation was that the LUP and ML problem are inherently the same. Both requires that an event e₁ is followed by an event e₂ on a feasible execution path for the same object. However, it is not the case. LDV and EV both perform poorly on the ML problem. The difference is especially pronounced for EV. It can check 99.3% LUP instances but only 37.5% ML instances. The evidence produced by EV is extremely valuable to gain insights into failures and improve the model checker. An analysis of the failures and targets for improving are presented in [33].

The results for LUP are reported in Table 1. The last two rows provide respectively the totals and the cumulative percentages for all three versions. EV performs significantly better than LDV as evidenced by the 99.3% Lock instances verified by EV. Also, EV finds the bugs missed by LDV. EV shows that the large number of potential bugs reported by LDV are actually not bugs.

The results for verifying the Memory Leak problem are reported in Table 2. The version (3.17-rc1) has 12.3 MLOC and 571, 012 functions. We did not verify the other two versions that were reported in Table 1 because of the significant difficulties we have faced in getting the LDV and EV tools to complete the verification on a majority of the memory allocation instances.

Using Evidence for Ease of Certification: The evidence produced using CE schema can reduce the efforts for the certification authority. Succinct visual evidence would definitely reduce the effort. Moreover, there are other ways the evidence can help in reducing the efforts. This case study presents a way to reduce the efforts.

A safety or a security property can have thousands of instances as evidenced by the Linux case studies. Each instance must be verified. The instances can have different kinds of and varying degrees of difficulty. For certification, it can be meaningful to categorize instances that have similar difficulties. The categorization can significantly reduce the effort for the certification authority and thus favor the use of mathematical analysis.

The first categorization is: whether the CF path feasibility check is needed and the difficulties of the check. It isolates the instances that require the feasibility check. A feasibility check is: (i) intra-procedural, i.e. the relevant conditions are within one function, or (ii) iner-procedural, i.e. the relevant conditions are spread across multiple functions. The intra-procedural category is further subdivided into simple and complex. The simple means the feasibility check is completed, without a SMT solver, just by using a few simple rules. The second categorization is: whether the verification intra-procedural or inter-procedural.

The results in Table 3 illustrate two categorizations. Note that only 4.4% LUP instances in the studied Linux versions require inter-procedural verification. Only 0.1% LUP instances require a complex intra-procedural path feasibility check and 0.2% LUP instances require an inter-procedural path feasibility check.

4.2 A Bftpd Case Study

Bftpd is a lightweight FTP server widely used in desktops, servers, embedded devices, and media centers. The 2019 paper [16]³ reported a memory leak in version 4.6 of Bftpd [4]. The paper [16] notes that it is a high severity vulnerability that an attacker can utilize to launch denial-of-service attacks. The vulnerability is assigned the CVE ID (CVE-2017-16892) and the Bftpd developers have issued a patch.

³ This paper is about detecting memory leaks using SAT solvers; it got the Distinguished Paper Award in May 2019 at the 41^st International Conference on Software Engineering

In this case study we show that the use of the CE schema leads to critical evidence that the paper [16] has missed. The critical evidence shows that the argument about the CVE in the paper is incorrect, and the detected memory leak is a false positive. Let us explain the critical evidence and how it counters the argument in the paper [16].

The paper [16] argues the following memory leak: the function command_rnto calls the function bftpd_cwd_mappath which allocates memory and returns a pointer to the allocated memory to command_rnto. As shown in the PCG in Figure 4(b), command_rnto does not free the allocated memory on path numbered 3. The paper [16] claims that the path 3 is feasible and thus it is a memory leak.

Let us now get to the first piece of the critical evidence that brings out issues with the above argument. As per the CE schema, every function f that calls bftpd_cwd_mappath is relevant because f gets the pointer to the allocated memory. The EV model checker yields 14 such functions as shown in Figure 5. Since each of these functions can produce a memory leak, each must be verified. The paper [16] argues about one such function, namely command_rnto. If we examine command_rnfr, another such function that calls bftpd_cwd_mappath, it also has a memory leak on the paths numbered 1 and 2, as shown by its PCG in Figure 4(a). At this point it appears as though the paper [16] has missed this other leak. However, the next evidence gives an interesting twist to the argument.

The next critical evidence shows that the memory leaks are false positives. Because of the space limitation, we provide only a piece of the next critical evidence that brings an interesting twist to the argument. The 14 functions that call bftpd_cwd_mappath are themselves called using function pointers by the function parsecmd (parse command). For example, if it parses the command RNTO (rename to), parsecmd invokes command_rnto. This parsecmd function includes an FSM that regulates the sequences of commands that would be allowed to execute. The FSM ensures the protocol: an FTP client must issue an RNFR (rename from) command to specify the original file name to be renamed followed by the RNTO (rename to) command to specify the new file name. If RNTO is not preceded by RNFR, parsecmd gives an error message instead of executing RNTO. This regulation prevents the memory leaks reported in the paper [16] because if RNFR is called before RNTO then the path numbered 3 in Figure 4(b) is not feasible and thus the reported memory leak cannot happen. The patch that the developers have added has actually undesirable side effects.

To conclude, since the CE schema is designed to look for exhaustive evidence, it helps in judging whether the evidence is complete and thus avoids pitfalls in making safety arguments. The completeness of evidence is clearly an important consideration for certification.

.

5 Conclusion

Software model checking is the algorithmic analysis of programs to prove properties of their executions. The paper introduces Certification Evidence (CE) schema to present evidence for the purpose of certification. For a succinct representation, the scheme unifies micro and macro evidence. The micro evidence shows that the control flow paths within a function are grouped into different groups for the purpose of verification. The macro evidence shows interactions among functions for the purpose of verification.

The paper presents Linux kernel case studies and a case study concerning a high severity memory leak vulnerability (CVE-2017-16892) in Bftpd software. The case studies illustrate the applicability and importance of the CE schema for verifying large real-world software.