Path Algebra for Scalable and Transparent
Software Security

1 Introduction

1.1 Fundamental Challenge: The Soft Infinity of Execution Behaviors

After grappling with a plethora of task-specific (analysis vs. transformation vs. verification) and language-specific software challenges, we believe the fundamental scalability challenge is rooted in the soft infinity of execution behaviors. The term soft infinity means a number so large (e.g., the estimated number of atoms in the universe) that it cannot be enumerated no matter how fast the computer. With just 100 nodes and 200 edges, the number of paths in a directed acyclic graph (DAG) can be soft infinity. The soft infinity of execution behaviors grows far beyond the paths in a DAG because of the program loops (even assuming all loops halt) and inter-procedural execution. The soft infinity of execution behaviors persists irrespective of the programming language and whether in source or binary form; it is a barrier that cannot be removed by good programming practices.

1.2 A New Approach: Path Algebra

We have been working on maintenance and evolution of large software since 1996. For the last 15 years, our efforts have been aimed at scalable and transparent technologies for analyzing, modifying, and verifying large software (e.g., Linux kernel with 25 million lines of code).

Recently, we have developed a novel non-commutative ring [1] for modeling execution behaviors, which we call the path algebra. By providing a compact representation of the soft infinity of execution behaviors, the path algebra enables scalable software analysis, modification, or verification. It can also provide transparency (i.e., ease of understanding) by retaining a direct correspondence to software and its control flow graph.

The path algebra has evolved from our last 15 years of experiments to solve the scalability and transparency problems we have encountered in working with our worldwide customer base which includes all major automobile, avionics and defense companies, and several DARPA cybersecurity projects. To facilitate fast iteration of non-trivial experiments with large software, we have built a sophisticated platform, Atlas [2, 3, 4], to build tools to analyze and modify software in C, C++, Java, Simulink, Java byte code, and binary. Atlas implements the eXtensible Common Software Graph (XCSG) schema [5], an eDSL for interacting with XCSG, extensive visualization to facilitate program comprehension, and a graph database to support fast execution of the eDSL on large software. The path algebra is aimed at addressing the limitations of several other techniques we have experimented with to manage the soft infinity.

2 A Motivating Problem

Before getting into the mathematical description of the path algebra and its use in practice, we need to tell a short story about the scalability and transparency limitations we encountered in a Linux verification experiment using the BLAST model checker [6].

This experiment sought to verify the safety property that a mutex LOCK is always followed by a mutex UNLOCK. The experiment involved 66609 LOCK instances. The limitations we encountered:

• Scalability Limitation of the Model Checker: The model checker could not complete the verification of 34% of the LOCK instances. It kept running without completing the verification.

• Transparency Limitation of the Model Checker: Here the transparency limitation showed up in two ways:

  • The model checker did not give any explanation for failure to complete the verification for some LOCK instances. Without a transparent reason for its scalability failure, one is handicapped in improving scalability.
  • For the instances the model checker pronounced safe (the safety property holds for all execution behaviors), the model checker did not give any information that humans can use to easily cross-check and reaffirm the validity of the answer.

The model checker verification is based on SAT solving which employs low-level Boolean logic abstractions for automated verification. The voluminous Boolean logic representation of the problem is not amenable to transparency.

Because of the lack of transparency, we adopted a different approach. We analyzed the control flow graphs (CFGs) and the call graphs (CGs) of the 34% of LOCK instances that could not be verified by the model checker. Often these graphs are very large and complex. To simplify and scale the graph-based analysis, we developed a graph dominator-based simplification for CFGs called the projected control flow graph (PCG) [7] and invented the technique of matching pair graph (MPG) [8] to enable scalability. We used the Atlas platform to build the PCG and the MPG based graph analysis tools. Our analysis led to a novel graph-based software verification technique that we used to complete the Linux verification [6]. The Linux verification result is publicly available through the website [9]. Through the supporting evidence we provide, our automated verification can be easily cross-checked manually for each instance.

3 Path Algebra

As noted earlier, we have been doing experiments for the last 15 years in search of a scalable and transparent technology for analyzing, modifying, and verifying software. The path algebra has resulted from the insights gained through these experiments.

3.1 Using Mathematics to Address Infinity

Our goal is to enable efficient analyses and transformations of software abstractions by managing the complexity caused by the soft infinity of execution behaviors.

Mathematics has a long history of addressing infinity with powerful concepts that in turn result in major scientific advances (e.g., Newton’s calculus based on infinite power series, Dirac’s Delta function that approaches infinity at a point). An appropriate concept can be the key to dramatically reducing the amount of computation to solve a problem that seemingly requires a soft infinity of operations. For example, the 2^100th Fibonacci number can be (unexpectedly) computed using 100 arithmetic operations using the golden ratio.

3.2 Defining a New Algebra

Abstract algebra provides the triumvirate of “Group”, “Ring”, and “Field” as foundational templates for the creation of new algebraic systems tailored for solving various kinds of problems. The path algebra is a novel algebra based on a non-commutative ring for modeling execution behaviors. In the path algebra, execution paths appear as products of variables. Addition describes branches. Loops succinctly appear as divisions with the loop bodies represented only once.

This new algebraic machinery is built using SymPy [10] and installed as a plug-in module in Atlas [2]. Our implementation is robust enough to process large software such as Linux kernel and supports several programming languages. We shall give an example to illustrate the path algebra followed by some highlights of our new findings using the path algebra.

Figure 1 illustrates how the path algebra can be used to verify a safety property - LOCK must be followed by UNLOCK on every control path. The example also brings out the use of homomorphism to distill relevant behaviors. The source code in Figure 1 models an example of a LOCK-UNLOCK bug we found in the Linux kernel [6].

Let’s explain some important points summarized in Figure 2:

1. Algebraic Representation of Execution Behaviors:
   • The totality of execution behaviors is represented by an algebraic compact representation of behaviors (CRB): B 2(3(T)4 5(F)8(10(T)11 + 10(F)13))^*(3(T)4 5(T)6 + 3(F))E where line numbers are used as IDs for the program statements. For conditional statements T and F represent True or False. The expression shows: 3(T) is followed by 4 and 3(F) is followed by E (i.e., Program End).
   • The compactness of CRB is due to algebraic factorization. When multiplied out, we get many monomials, each for one execution behavior. For example, the monomial 2(3(T)4 5(F)8 10(T)11)^*3(T)4 5(T)6. It is the behavior when the while loop iterates with 5(F) and 10(T) for every iteration, followed by break.
   • The execution behaviors due to a loop are given by a subexpression that is superscripted by the * operator for iterations of the behaviors represented by the subexpression.
2. Homomorphism for Relevant Execution Behaviors:
   • Homomorphism is a powerful tool in abstract algebra. It is used here to extract execution behaviors that are relevant for checking whether LOCK (line #4) is always succeeded by UNLOCK (line #8).
   • Execution behaviors extracted by the homomorphism are given by: (3(T)4 5(F)8 )^*(3(T)4 5(T) + 3(F)).
3. Software Verification Using Homomorphism:
   • Among the two extracted behaviors, there is one in which LOCK (line #4) is not succeeded by UNLOCK (line #8): (3(T)4 5(F)8 )^*3(T)4 5(T)
4. Algebraic Representation of Execution Behaviors of a Loop:
   • The algebraic expression represents the three kinds of behaviors for a loop: iterative behaviors with the normal exit from the loop (3(F) in the example), terminal behaviors resulting in an exit from the loop (5(T) in the example), and the behaviors when the loop is skipped (* can be zero iterations).
   • Interestingly, path algebra captures a loop by a division operation and the resulting fraction turns out to be a closed-form expression for an infinite geometric series that we can relate to the iterations of a loop. In the algebraic derivation, we get the fraction 1​1 − S for execution behaviors of a loop that are associated with the subexpression s.
   • In presenting an algebraic expression we write s^* for 1​1 − S as the * operator is a commonly used notation to represent iterations.

3.3 Derivation of the Compact Representation of Behaviors (CRB)

Given a directed graph G, the algebraic expression is derived by setting up a linear system of equations S that uniquely captures G. The path algebra is defined on edges where multiplication stands for concatenation of paths and + stands for union of paths. Each node i in G is assigned a variable X_i. The coefficients in a linear equation are identifiers for edges. On solving the equations, we get a subexpression as the value for each X_i. The subexpression gives the set of paths from the root (node #1) to node i.

Figure 2 shows a simple graph with a loop, the corresponding linear system of equations, and the answer obtained by solving the system of equations. Note that we first obtain the subexpression as a product of edges. Since the edges are for the successor relation [11], the subexpression is called the compact representation with successors (CRS). The CRS is converted to CRB by mapping each edge to its tail node. As noted earlier, the loop is captured by a division operation.

4 Benefits of Path Algebra

4.1 Scalability for Software Security

The foremost important benefit of the path algebra is the scalability it provides to ensure software security. A security property must be checked for every execution behavior. A check by enumerating behaviors is often impossible because of the soft infinity of execution behaviors. Recall the earlier illustration of the path algebra to check whether LOCK is always followed by UNLOCK. By providing a compact representation for all execution behaviors and the use of homomorphism to easily extract the relevant behaviors, the path algebra makes it possible to check every execution behavior without enumerating behaviors and that drastically reduces computation for checking software security properties.

4.2 Transparency for Software Security

As noted in the Linux verification experiment, the model checker does explain the model checking steps. Those steps involve low-level abstractions and voluminous details that are not amenable to human understanding. In their landmark paper [12], De Millo, Lipton, and Perlis (recipient of the first Turing Award) argue that automated software verification should follow the example set by mathematics to create proofs amenable to human understanding.

The path algebra provides a compact representation with direct correspondence to execution paths that humans can easily relate to. Algebraic homomorphism further elevates human understanding by enabling the focus on relevant behaviors. Let’s exemplify by revisiting the example in Figure 1. The homomorphic expression for the execution behaviors that violate the safety property is: (3(T)4 5(F)8 )^*(3(T)4 5(T) + 3(F)). It is easy to see that the violation of the safety property occurs exactly when the conditions at line 3 and 5 are True, leading to a LOCK which is never followed by an UNLOCK. Equipped with this information humans can easily cross-check the verification without getting entangled into the multitude of execution behaviors.

5 Far Reaching Insights and Applicability of the Path Algebra

Figure 3 shows the control flow graph of a code segment with GOTO statements. It involves LOCK (L) and UNLOCK (U). Is L followed by U on all execution paths? Note the complexity of the graph. Some may call it spaghetti code. Can the path algebra characterize the complexity of spaghetti code? Can the path algebra manage the complexity and enable scalable and transparent analysis of security properties?

The complexity in Figure 3 is not just about a theoretical curiosity. We often encounter it in the implementation of a complex finite state machine (FSM) and then it is important to know whether the machine has weird (unintentional) behaviors. Linux kernel has thousands of GOTO statements. Are they barriers to verify security properties? Should Linux be rewritten to remove GOTO statements? Can the path algebra help in rewriting the code? Linus Torvalds has opposed such rewriting [13]. Can the path algebra provide insights to help us understand why or why not GOTO statements should be used? Understanding and managing of the complexity of GOTO (jumps) is a must for binary.

We will bring out the insights and the applicability of the path algebra in the following order:

A. The path algebra provides a surprising and quantitative characterization of the complexity due to GOTO. Note that many luminaries in computer science have wrestled with this problem and that resulted in the invention of so-called structured programming. In his paper [14] titled “Structured Programming with GOTO Statements,” Knuth summarizes his discussions with Dijkstra, Hoare, and others with the conclusion: “Everybody knows it (structured programs) is a Good Thing, but as McCracken has said, few people would venture a definition. In fact, it is not clear that there exists a simple definition as yet.” Knuth and Floyd [15] have tried to formulate a characterization based on regular expressions. In our communication with Knuth, we have discussed how the path algebra is crucial to resurrect their attempt.

B. The path algebra leads to canonical transforms to eliminate GOTO statements. Manna wrote the book [16] “Introduction to Mathematical Theory of Computation,” and later applied the theory to develop a systematic method to eliminate GOTO statements [17]. The path algebra is much simpler and more elegant than the mathematical theory proposed by Manna.

C. In practice (e.g., GOTO in Linux) the complexity can be directly managed by the path algebra. There is no relief given by structured programming because eliminating GOTO creates another complexity. Thus, the path algebra is especially important for binary analysis where eliminating GOTO (jumps) is not an option.

5.1 Algebraic Characterization of Structured Programs

The theorem proved by Böhm and Jacopini [18] became the cornerstone of the structured programming gospel by Harlan Mills at IBM [19]. Dijkstra invented the term structured program for a class of GOTO-less programs [20]. We use the term structured program for the class of defined by Dijkstra. Recall we introduced CRB and CRS as two the forms of compact representations for execution behaviors. The CRB is the representation using the nodes and CRS is the representation using the edges of a control flow graph. We can define “structured” using CRS:

A program is structured if and only if the CRS has no repetition of edge elements.

Coming back to the control flow graph in Figure 3, the CRS is:

Repetitions: e₅: 2, e₆: 4, e₈: 2, e₉: 4, e₁₃: 2, e₁₄: 2. The number of repetitions quantify the unstructuredness.

5.2 Canonical Transformation for Deriving GOTO-less Programs

Manna wrote the book [16] “Introduction to Mathematical Theory of Computation,” and later applied the theory to develop a systematic method to eliminate GOTO statements [17]. Let’s illustrate how the path algebra leads to a simple, elegant, and powerful framework for transforming an unstructured program to a structured program.

Figure 4 shows the control flow graph (CFG) of an unstructured program and the CFG of its structured transform. Earlier literature including Manna describes unstructuredness as violation of either unique entry or unique exit of a control block. First, note the duality of unstructuredness brought out by the path algebra where the same unstructuredness appears as either multiple entries or multiple exits depending on the choice of the control block (shown as the shaded block). This duality corresponds to two ways to factorize to avoid the repetitions of edge elements. Recall that such repetitions characterize unstructuredness. As shown in Figure 4, the algebraic expressione₁e₂e₃ + e₁e₄e₅ + e₆e₅ for the execution behaviors can be factored in two ways: (i) e₁(e₂e₃ + e₄e₅) + e₆e₅ to avoid the repetition of e₁ (we call this a prefix repetition), or (ii)e₁e₂e₃ + (e₁e₄ + e₆)e₅ to avoid the repetition of e₅ (we call this a postfix repetition). The duality leads to two canonical transforms shown as Transform-1 and Transform-2. Note that both the transforms eliminate the unstructuredness by replicating the repeated edge element and that requires replication of code. For example, the code A₄ is replicated and shown as A₄₁ and A₄₂ for Transform-1 and the corresponding replication of the edge element e₅ is shown as e₅₁ and e₅₂.

5.3 Managing the Complexity of GOTO with Path Algebra

Using the transformations discussed above, one could eliminate GOTO statements. However, there is a cost to pay for eliminating GOTO. Note that the transform involves replication of code which is contrary to the soft engineering dictum that advocates reuse of code. Thus, algebra clearly brings out that structured vs. unstructured is really about the trade-off between replication vs. reuse. Sometimes the application logic is inherently unstructured (as is the case with some FSMs) and writing a structured program cannot get rid of the complexity–it simply reenters in the form of replication. While Linus has not articulated his reasons to use GOTO, the path algebra helps us understand and support his position.

The example in Figure 3 looks complicated. As noted earlier, the CRS has repetitions. Eliminating the GOTO involves many replications of code; the code becomes verbose but not any easier to understand. Despite this, the complexity can be directly handled by the path algebra because deriving and analyzing the CRS does not change because of repetitions–it is equally straightforward to apply the homomorphism to derive relevant behaviors.

As shown in Figure 3, the homomorphism maps the CRS to:

The resulting algebraic expression makes it very transparent that L is not followed by U when the loop ends with behaviors: e₇e_Le₈e₉ or e₇e_Le₁₄e₆. With the help of the path algebra, it just takes a quick glance to cross-check the answers.

6 New Research Directions

Many software abstractions are naturally expressible as graphs (e.g., the dataflow graph, the control flow graph, the call graph). The algebraic approach leads to many new research possibilities as the approach is equally and widely applicable to various graph-based abstractions.

For an automobile company, we have developed a tool to verify control-flow based equivalence between the C source and the PowerPC binary. Subsequently, we conducted a similar experiment with an open-source operating system and reported the findings in a paper [21]. This experience suggests a new research direction to check the sanctity of the build process.

The path algebra can be applied to investigate a variety of software abstractions. For example, for scalable and accurate dataflow analysis without getting entangled in the state space explosion.

Another interesting research would be to explore the use of algebra to address the scalability and transparency issues for SAT solvers. Our preliminary experiments lead us to believe that a special algebra can be developed for a scalable and transparent solution framework for the 3-SAT problems.

7 Appendix: Using Atlas to Investigate BLAST Linux Analysis

As mentioned earlier, we used Atlas to conduct experiments to investigate transparency and scalability issues we encountered in the BLAST verification results, and to later help us complete the Linux verification for the 34% LOCK instances that could not be completed by BLAST .

We categorized the LOCK instances that could not be completed by the model checker. An example of the ATLAS script for the categorization is shown in Figure 5; it illustrates how one can write a compact eDSL script to identify a complex category where the LOCK and UNLOCK instances are in different functions and those functions are called in a loop. Figure 5 shows a part of the script that obtains all loops containing a function call; the use of XCSG tags such as XCSG.Loop and XCSG.LoopChild helps keep the query succinct. The source code in the illustration is a toy example (foo and bar). However, the same query can be run on large software with millions of lines of code to extract quickly all the LOCK instances belonging to the category.

Secondly, we illustrate the use of Atlas to do experiments with the path algebra. To gain insights, we performed path algebra experiments with XINU [22], a small operating system. We computed path expressions for the control flow graphs of all XINU functions.

Figure 6(a) shows the source code for the function blkcopy in XINU. Figure 6(b) shows the corresponding control flow graph (CFG). Figure 6(c) shows the edge labels e_i and node labels X_i for the CFG. The linear system of equations is set up using e_i and X_i. Figure 6(d) shows the XCSG eDSL queries and the results. The query getEquations creates the linear system of equations for the labeled CFG, and the query getCRS computes the CRS by solving the equations. The first query is to get the node for the function blkcopy and store it in a variable named blkcopy. The variable is used as the input for the subsequent queries.

Note that Atlas stores the entire program as a graph called the Universal Graph. Program artifacts such as functions are stored as nodes with XCSG-attributes relationships between program artifacts are stored as edges with XCSG-attributes. Several data and control flow relationships are precomputed by Atlas and the results are stored in the Universal Graphs. eDSL queries access the Universal Graph.

eDSL is a DSL embedded in Java. The queries shown in Figure 6 can be embedded in a Java loop to compute the CRS for all the 210 XINU functions, altogether 11000 lines of C code. The CRS for all the XINU functions can be computed in less than a minute on a laptop.

7.1 Linux Verification Experiment

Earlier we have discussed the Linux verification experiment. The table in figure 7 provides a summary of the results of the experiment.