The Logika Verification Framework

To support developer-friendly Slang verification, Logika provides code-level IDE integrated verification of Slang’s contract and proof languages.

Verification is highly automated by using a suite of state-of-the-art SMT solvers that work in the background to provide continuous delivery of program checking.

This continuous, always on, verification is enabled by a significant tool engineering effort. In particular, Logika is able to provide smart incremental checking that is triggered by editor actions by maintaining behind the scenes a sophisticated map of program dependences.

This incremental checking is key to scalability. When updates are made in the editor, it enables Logika to re-check only the code changed as well as other code that depends on the changes.

Scalability is also enabled by a powerful server-based architecture that provides massive parallelization of the formal verification. This provides a foundation for scalable cloud-based delivery of verification resources for on-demand servicing of verification needs.

Finally, since we realize that not all verification can be automated, Logika provides what we call deep-dive gateways in both the verification tool and in the proof notations to allow expert-level engineers to drill down into verification details and to introduce manual proof engineering when needed.

Intellij provides extension points for customizing its Scala type checker, so we can adapt it to work nicely with Slang.

Slang analysis engines, such as Logika, runs as a Sireum micro service in the background.

Here, we have some example code with data structures inspired from an unmanned aerial vehicle mission control system.

The example declares an immutable Waypoint datatype that holds coordinate information.

A mission typically consists of a sequence of waypoints such as what is stored in S one, which is of mutable sequence type.

As Logika works, it decorates program editors to communicate its analysis feedback.

It decorates each statement with its precondition state claims that it computes, which aids program reasoning while also serving as auditable evidence.

The state claims are naturally represented at the Slang source level, and as you can observe, the claims are intuitive as there is no heap object representation, pointers, or references.

This is the direct result of Slang language simplification, which both reduces our reasoning mental model burden and helps scale Slang analyses

Logika also decorates the editors with verification condition checking results, in this case, by using SMT query solving.

Each query is annotated with solving result, as well as its solving parameters, which can be configured by users.

Each sequence or array access is implicitly bound-checked to ensure that it does not produce runtime error or buffer overflow.

Suppose that we seed an out of bound access. Logika analysis in the background continuously give direct verification feedback upon code change.

We believe such seamless integration into typical development workflow is key to formal method success.

As issues are fixed, Logika re-verifies the code and can confirm that such issues have been properly addressed.

We like this line editor decoration feedback mechanism because it gives a sense of analysis coverage, which feels familiar to the line coverage information in testing.

Let us now start adding some explicit assertions to confirm our understanding of the program behaviors. For example, we can assert that the first element of S two is a waypoint holding the coordinate one, two, and three, as assigned at line fourteen. Obviously, such assertion should hold and it is confirmed by Logika as the feedback decoration does not indicate that there is an issue.

Suppose that we assert the same for the first element of S one. This is where Slang differs from Scala or Java where a deep copy of S one was made at line eleven before assigning to S two. Thus, the assertion is invalid

We can confirm such behavior by running the program, by clicking the green play icon at the top of the program editor, and it will trigger code compilation. Once it finishes, the resulting code is then run, which in this case, triggers an assertion error, as Logika has warned us. This illustrates how one can test and prove their code in the same Sireum verification environment.

Due to the deep copy, the value of S one should not be affected, and it is the same as what assigned at line ten.

We can ask Logika to confirm it for us by asserting it.

One might think that such deep copying might produce less than ideal performant code, however, in many cases, the performance differences do not matter as much as what we might have thought.

On cases where they do matter, there are effective programming patterns and principles that can be applied, which are discussed in the Slang Isola paper appeared last year.

Let us now look at more interesting properties.

I am going to copy and paste some prepared code to save time.

You can observe that the added methods have some contract annotations.

Both inZone and W P diff are strictly pure methods, which do not make side effects. Such methods can be directly used in contract specifications, as shown in move waypoint X, which has the typical pre and post conditions.

Move waypoint X itself is a pure method, which means that there is no observable side-effect from the outside of the method.

As can be observed, we leverage Scala syntax to express specification. The Contract specification at line 28 is implemented by using a Scala macro which is erased before code generation, thus, the specification does not affect the code runtime behaviors.

In the future, it is possible to introduce a runtime assertion checker tool that weaves in contracts as assertions for testing purposes, or dynamic enforcement

Now let’s consider the theme of incremental checking by discussing some of the details of the Sireum code base.

Up to this point, we’ve been demoing Slang and Logika on some small script files. So you may be wondering, does all of this work “at scale”? The answer is Yes! In addition to applying Slang and Logika with our industrial partners on various DOD projects, we also validate the design and scalability of Slang and Logika by applying them when developing the Sireum code base itself, which is around 210,000 lines of code.

One interesting thing to note is about 85 percent of the code base, around 180,000 lines of code, is written in Slang.

So not only does that validate the effectiveness of Slang for coding large applications, it means that we can also apply Logika to verify portions of the Sireum code base, including our HAMR code generation pipelines for SEL4 as well as the Logika implementation itself.

This provides a pathway for eventually mechanizing the proofs of correctness of our own verification analysis and code generation tools. We’re currently applying these idea to HAMR infrastructure code generated for SEL4.

We believe that this may eventually be helpful with tool qualification.

We’re now going to demonstrate that the same continuous integrated verification that worked for small programs also works when Logika is applied to this large code base. This is possible due to our carefully engineered approach for incremental checking.

Let’s jump into the middle of the Slang code base, and look at the implementation of the option type. Option is part of the Slang runtime library that is part of the large Sireum codebase.

Here you can see that the Slang implementations include some very basic contracts.

For this example, the size of the contract and associated code is not important. Slang does not have null value to avoid the billion dollar issues associated with it, thus, option should be used instead.

To reduce memory overhead at runtime, the Slang compiler plug-in for Scala optimizes away options inside object internal representations.

Option is part of the Slang runtime library that is part of the large Sireum codebase.

The main point is that Logika verification will be triggered by edits in the file to start the checking process. Then, the Logika incremental analysis framework will scan the dependence information for the entire code base and figure out that the effects of the edit that we are making are confined to the body of this method.

You just saw a moment ago that Logika was able to quickly conclude its checking to find a contract violation in less than a second.

Then, when we correct the error, Logika can conclude almost immediately that method satisfies its contract. Moreover, due to the dependence analysis, Logika has already confirmed that the rest of the codebase has been unaffected by the edits and thus all of the specifications throughout the rest of the code remain satisfied.

Logika incremental checking leverages project codebase modularity for scaling its analysis and optimizing user interactions.

Just like a compiler, it understands the dependence relationships between modules as captured in the system’s build specification. For example, the modules and dependences reflected in the Sireum code base build specification are diagrammed below.

Beyond this, Logika adds additional finer-grain dependence analysis based on call graph constructions.

Using this information, when a file is edited or a current point in the program is selected for verification, Logika can avoid examing code not needed for the verification of the current section of code.

Let me describe how it works, intuitively.

When a particular file such as Option is analyzed Logika starts at the root modules and works downward in the project module dependency graph. until it finds the module where the file resides.

Along the way, Logika only lightly analyzes the relevant modules.

That is, Logika employs the Slang frontend to parse and outline class, field, and method type signatures for all files in the modules, without fully type checking method bodies.

Only the Option file is fully type checked, which then verified.

In the context where user is editing a particular method, the process is further optimized by focusing full type checking and verification to that method.

Furthermore, Logika aggressively caches intermediate analysis results to speed up subsequent analyses. For example, module-level file type information is soundly cached by file fingerprinting.

SMT queries are also cached to speed up re-verification. We found these to be very effective, especially so for providing continuous verification in an IDE.

For less capable machines, Logika offers ways to tone down its caching strategies.

Let’s now consider the Parallelization and Server-based Deployment theme.

One key observation is that, as Logika works over the project module dependency graph, modules that are at the same depth level can be verified independently in parallel.

Moreover, Logika’s reasoning is compositional, thus, each program unit such as a method, or even each contract case of a method, can be verified in parallel.

In the future, it is also possible to verify all project modules using different computing nodes, for example, in a cloud infrastructure to provide continuous verification with on-demand scaling of resources.

In such setup, each computing node can also provide parallel verification.

We believe parallelization and distributed analyses hold a great promise to help tackle scalability issues in applying formal methods.

It is especially so when considering the trend towards remote development using a thin client, or even a browser that only requires a minimal setup.

This strategy is often used to ensure the integrity of the development tool chain or to avoid leakage of intellectual property that might occur when code bases and tool chains are installed on individual machines in possession of employees.

Now, allow me to demonstrate with an i-pad as a thin client connected to a server with 80 cores.

Here is an i-pad with the Safari browser on the left-hand side.

The browser is connected to a headless instance of the Intellij based Sireum integrated verification environment, running on one of our research group’s Linux servers at K-State, called legion.

That is, the headless Sireum server in legion projects its graphical user interface through the usual web protocol, thus, any authenticated machine with a browser can be used to interact with it.

This particular demo uses the building temperature control example generated by hammer, with gumbo contracts presented earlier already translated as Slang contracts.

On the right-hand side is a terminal connected to legion, which is used to display legion’s C P U and memory loads using H top.

As can be observed, legion has eighty cores with two terra-bytes ram.

Next, I will open the temperature controller component implementation, which will trigger Logika verification, and you can observer how Logika put legion’s many cores to work.

As can be observed, Logika parallel verification engine used as many cores as needed for analyzing large codebases.

In closing.

Finally, for the proof-engineering theme we are not claiming to do anything significant from a theoretical point of view.

However, in practice, we believe our approach for supporting proof scripts and manual proving steps directly in Slang has some advantages.

Here we see how we exploit Scala’s syntax flexibility to also express proofs directly in the program. Some of the proof steps illustrate how we use Slang pure methods to represent lemmas and theorems.

Because all the proof elements are first-class citizens in the programming language, Intellij refactoring works for Slang proofs as well.

After the refactoring, Logika ree checks the proof to make sure that it is still admittable.

The numbering does not have to be in order, which is sometimes handy. We do offer an automatic tool renumbering to tidy up Slang proof.

Each proof step in Slang has to be justified, and the justification implementation should produce an understandable explanation on why it accepts the proof step’s claim.

Logika provides an extensible facility to add and define justifications.

For example, for the premise justification, the implementation informs the user that either the proof step’s claim is derived from the previous context or where it has been previously proven.

The premise justification is actually a method signature declaration, whose implementation is provided via a Logika plug-in written in Slang.

Custom justifications that implement complex proof tactics can be defined using this extension mechanism. Thus, to keep with our deep-dive gateway theme, while we advocate interactive theorem proving to be done directly in Slang so that we have continuity of user experience, custom justifications can be introduced to export Logika’s verification conditions for expert users to other theorem prover’s input language.

Note: “continuity of user experience” - Kathleen Fischer used this phrase, so I suggest we use it verbatim, such as for Isabelle, Coq, or A C L two.

Justifications can also be provided by applying lemmas or theorems, such as the and elimination one theorem that is automatically proven using SMT solving.

Note that these lemmas and theorems are Slang pure methods, thus, they are allowed to make local side effects that are non-observable from outside the methods. This means that one can use loops or recursion to crawl complex structures as part of the proving process. Such iterative and recursive structure crawling approaches correspond to inductive proofs, but expressed in more developer-friendly notation. Unfortunately, time does not permit a more detailed exposition on this interesting topic.

Logika uses a general tactic that we termed inception, to lift pure methods that may make local side effects, as logical lemmas and theorems and apply them.

Inception generates an understandable explanation that details the steps it takes for the lemma or theorem application.

It can also automatically infers lemma or theorem application arguments, and indicate such inference as part of the explanation that it generates.