CIS-5130 (Analysis of Artifacts) Home Page
This is the home page for Peter Chapin's CIS-5130 course notes for the Fall 2024 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
- 2024-08-26. Course introduction and overview.
- 2024-08-28. Introduced SPARK. Had a conversation comparing Rust and SPARK.
- 2024-09-02. No class (vacation).
- 2024-09-04.
Discussed the BinarySearch example. Illustrated loop variants.
- 2024-09-09. Discussed Homework #1. Discussed the
SelectionSort example that uses ghost functions.
- 2024-09-11.
Introduced Frama-C and ACSL.
- 2024-09-16. ?
- 2024-09-18. ?
- 2024-09-23. ?
- 2024-09-25. ?
- 2024-09-30.
Short discussion of how SPARK deals with memory safety (more discussion pending?) and other
topics.
- 2024-10-02. No class
- 2024-10-07. No class (Vacation).
- 2024-10-09. No class (Vacation).
- 2024-10-14.
Henry presented on Rust. Discussed on Rust's memory safety versus SPARK's.
- 2024-10-16.
Discussed the Splint paper with a demonstration of Splint.
- 2024-10-21. A
conversation about Rust and a Frama-C demonstration.
- 2024-10-23. Discussed secure information flow.
- 2024-10-28. A
brief discussion of MIRAI (for Rust), followed by a discussion of ASIS, libadalang, and ATC.
- 2024-10-30. ?
- 2024-11-04. ?
- 2024-11-06.
Demonstrated Frama-C, and it's GUI, Ivette, in the context of Homework
#2
- 2024-11-11. Conversation about Homework #1 and Homework #2.
- 2024-11-13.
Discussed Frama-C's metrics and slicing plugin. Discussed call graphs, stack analysis, and
cyclomatic complexity.
- 2024-11-11. Discussed code coverage and gconv.
- 2024-11-13. Discussed execution profiling and gprof.
- 2024-11-18. No class (Vacation).
- 2024-11-20. No class (Vacation).
Slides
Papers
A detailed bibliography in BibTeX format.
- Static Detection of Dynamic
Memory Errors by David Evans
- Improving Security Using
Extensible Lightweight Static Analysis by David Evans and David Larochelle
- An
Introduction to Memory Safety Concepts and Challenges by Forough Goudarzi, November
10, 2023 (on the AdaCore Blog).
- Using Pointers in
SPARK by Claire Dross, June 6, 2019 (on the AdaCore Blog)
- Memory
Safety in Ada/SPARK Through Language Features and Tool Support by Forough Goudarzi,
November 15, 2023 (on the AdaCore Blog)
- Memory Safety in Rust by Ben
Brosgol, January 29, 2024 (on the AdaCore Blog)
- 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.
Samples
Homework
- Homework #1. SPARK. This assignment gives you an
opportunity to experiment with SPARK.
- 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).
- Read the first Splint paper (Static Detection of...).
- OPTIONAL. Read the second Splint paper (Improved Security Using...).
- OPTIONAL. Read the Why3 paper (Why3: Shepherd Your Herd...).
- Review Rust's approach to memory management via its ownership model.
- Homework #2 gives you an opportunity to experiment with
Frama-C's WP plug-in and compare it with SPARK.
- 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.
- Try out the gcov demonstration sample.
- Try out the gprof demonstration sample.
- Read the paper Valgrind: A framework for....
Resources
The following are links to relevant resources for this class.
Last Revised: 2024-12-02
© Copyright 2024 by Peter Chapin
<peter.chapin@vermontstate.edu>