CIS-5130 (Analysis of Artifacts) Home Page

This is the home page for CIS-5130 course notes for the Fall 2019 semester. Here you will find class handouts, slides used during the lectures, homework assignments, and links to other references of interest.

The course syllabus gives an overview of the course and its content, lists course resources, and describes the grading policy and related issues.
The homework submission area and grade book are on Canvas but all other course resources are here.
Here is a list of the analysis projects chosen by the class members.

Topics

2019-08-27. Course introduction and overview. Introduced SPARK.
2019-08-29. Demonstrated SPARK using the Buffers example.
2019-09-03. Demonstrated SPARK contacts and loop invariants.
2019-09-05. Discussed the BinarySearch example. Demonstrated using SPARK on a larger example (CubedOS).
2019-09-10. Provided hints related to Homework #1. Discussed the SelectionSort example that uses ghost functions.
2019-09-12. Described in the architecture of SPARK and its use of Why3.
2019-09-17. Discussion of the first Splint paper, with demonstration.
2019-09-19. Discussion of SPARK's ownership model of pointers.
2019-09-24. Introduced Frama-C and the WP plugin for doing formal verification.
2019-09-26. Brief discussion of JML and the goals of the KeY project. Started discussing Frama-C's value analysis. Reviewed the EVA tutorial in the EVA documentation.
2019-10-01. Discussed Homework #3. Introduced the analysis project.
2019-10-03. Discussed software metrics and the Frama-C metrics plug-in. Discussed call graphs, stack depth analysis, and cyclomatic complexity.
2019-10-08. Discussed code coverage and gconv.
2019-10-10. Discussed execution profiling and gprof.
2019-10-22. Discussed valgrind.
2019-10-24. Discussed secure information flow.
2019-10-29. Discussed ASIS and libadalang.
2019-10-31. Discussed spin.
2019-11-05. Introduced the ELK stack.
2019-11-07. Discussed the RFC index example: indexing the RFC index in Elastic.
2019-11-12. No class.
2019-11-14. Introduced logstash.
2019-11-19. No class.
2019-11-21. ?
2019-12-03. Homework time.
2019-12-05. Homework time.

Slides

ASIS
ASIS Tutorial
ATC Presentation. Ada Taint Checker (ATC) is a tool I wrote (incomplete) for a UVM class in 2009. It uses ASIS.

Papers

A detailed bibliography in BibTeX format.

Why3: Shepherd Your Herd of Provers by Francois Bobot, et. al.
Static Detection of Dynamic Memory Errors by David Evans
Improving Security Using Extensible Lightweight Static Analysis by David Evans and David Larochelle
JML: a Java Modeling Language by Gary Leavens, Albert Baker, and Clyde Ruby
Preliminary Design of JML: A Behavioral Interface Specification Language for Java by Gary Leavens, Albert Baker, and Clyde Ruby
A Value Analysis for C Programs by Geraud Canet, Pascal Cuoq, and Benjamin Monate.
Structuring Abstract Interpreters Through State and Value Abstractions by Sandrine Blazy, David Buhler, and Boris Yakobowski
Valgrind: A Framework for Heavyweight Dynamic Binary Instrumentation by Nicholas Nethercote and Julian Seward.
A Lattice Model of Security Information Flow by Dorothy Denning.
A Primer on Model Checking by Mordechai Ben-Ari.

Samples

An example of a SPARK buffers package. This package provides a fixed length array type to hold characters and a collection of subprograms to manipulate such arrays. Two versions are provided: a version without postconditions and a version with postconditions.
An example of binary search in SPARK, with variations. This illustrates preconditions, loop invariants, loop variants, and generics.
A SelectionSort implementation in SPARK with proof of correctness.
A dynamic string type for C with Splint annotations.
A Binary Search Trees implementation in SPARK showing SPARK's upcoming support for access types. Compare with Splint's annotations for memory manage and with Rust's handling of memory management issues.
Some samples showing Frama-C's WP plugin in action.
The files used by the EVA tutorial in the Frama-C documentation.
A small demonstration of gcov that illustrates the code coverage of a few trivial tests of the str.c module.
A small demonstration of gprof that illustrates profiling a QuickSort implementation.
A small demonstration of valgrind that provides a simple (and short) application to analyze with the various valgrind tools.
A small demonstration of spin from the tutorial paper by Ben-Ari.
A small demonstration of the ELK stack that includes information on the RFCs. This can be used to populate an Elastic instance with an index of the RFC index.

Homework

Homework #1. SPARK. Due: 2019-09-13. This assignment gives you an opportunity to experiment with SPARK.
OPTIONAL. Read the Why3 paper (Why3: Shepherd Your Herd...).
Read the first Splint paper (Static Detection of...).
OPTIONAL. Read the second Splint paper (Improved Security Using...).
Review Rust's approach to memory management via its ownership model.
Set up Frama-C on Lemuria or on your own system. This entails installing OPAM and then using OPAM to install Frama-C and all its dependencies (which OPAM will figure out for you).
Homework #2 gives you an opportunity to experiment with Frama-C's WP plug-in and compare it with SPARK.
OPTIONAL. Read the two JML papers listed in the Papers section above. Review the KeY project.
Read the paper Value Analysis for C Programs.
Review the tutorial for Frama-C's EVA plug-in.
Homework #3 gives you an opportunity to experiment with Frama-C's EVA plug-in.
OPTIONAL. Read the paper Structing Abstract Intpreters...
You will do an analysis project of your own choosing.
Try out the gcov demonstration sample.
Try out the gprof demonstration sample.
Read the paper Valgrind: A framework for....
OPTIONAL. Read the paper Lattice Model of....
Import the RFC index into an Elastic instance. Use the sample RFC-0821 information as a basis.

Resources

The following are links to relevant resources for this class.

The SPARK Reference Manual.
The SPARK Users Guide.
The opam tool is used to manage OCaml packages, including the OCaml compiler itself.
Objective Caml is a programming language favored by those doing research in formal verification. It is also a good, general purpose functional/imperative/OOP language.
Why3 is an intermediate verification language.
SMT solvers: alt-ergo, cvc4, z3.
Proof assistant tools: Coq, Isabelle.
The Splint home page.
The Splint Manual.
Frama-C is a framework for the analysis of C programs.
ACSL by Example demonstrates ACSL on various "simple" C library-like functions. It can be used as a vehicle for learning ACSL.
The KeY Project provides formal verification of Java programs augmented with JML (Java Modeling Language) specifications.
Frama-C's slicing plugin documentation.
The Valgrind home page. A direct link to the Valgrind User Manual.
Jif is an extended version of Java that supports secure information flow labels. It is a research project at Cornell University.
Microsoft's Code Contracts allow any .NET language to benefit from contract style programming. The contracts are proved statically if possible, but failing that are tested dynamically.
Here is the GitHub site for AdaCore's libadalang library supporting the construction of Ada tools that need to access the parse tree of Ada programs.
The clang C/C++ compiler provides well documented interfaces to facilitate the creation of tools for analyzing C and C++ programs.
Roslyn is an open source C# compiler that provides rich APIs that allow analysis tools to access internal compiler information.
The spin tool does model checking.
The Elastic Stack.
The Alloy tools.