Program Analysis, Testing & Formal Verification :

Formal Method is a set of techniques and methodology that helps us in doing formal verification. Formal Verification is a way of defining a concrete / abstract overview of a problem or model and then answering some questions regarding the properties of that model. We try to prove certain assertions and check for validity. Eg. Given a program does it ever happen that some variables take negative values. Does a model access a particular array element while execution. Some of the claims and problems that verifications tries to solve are undecideable but these things are done in finite amount of time and resources for most of the practical programming/development problems that we try solving via abstractions and approximations. You can however provide specific inputs that make the problem hard to solve/non halting.

Figures

• Install and use inkspace to make beautiful drawings for your paper

ACM Winter School :

• ACM Winter School : Computer Architecture, Compilers, PL, Logic, Testing & Verification.

Research Papers & Topics

Some cool paper links.

[⬆] Paper Links

• [ ] KLEE Paper
• [ ] Deferred concretization in symbolic execution via fuzzing
• [ ] UCLID Paper
• [ ] Bucketing Failing Tests via Symbolic Analysis
• [ ] Hot Path SSA
• [ ] K-paths Profiling
• [ ] Exploring program phases for statistical bug localization
• [ ] Symbolic Execution and Dynamic Taint Analysis
• [ ] Non-Interference
• [ ] A Formal Approach to Secure Speculation
• [ ] A Formal Verification Framework for Security Issues of Blockchain Smart Contracts
• [ ] Formal Verification of Smart Contracts: Short Paper
• [ ] ZEUS: Analyzing Safety of Smart Contracts
• [ ] Using Dafny, an Automatic Program Verifier
• [ ] DART Paper
• [ ] From Program to Logic: An Introduction
• [ ] SAGE : Whitebox Fuzzing for Security Testing
• [ ] SoC Verification Problem

[⬆] Other Papers

• [ ] ConCert: A Smart Contract Certification Framework in Coq
• [ ] Scilla-Paper
• [ ] CUTE Symbolic Execution
• [ ] Control Flow Integrity
• [ ] Avoiding Exponential Explosion

Reading Material & Book References

• [ ] Dafny
• [ ] Hyperproperties
• [ ] Computer Security
• [ ] Dafny Examples
• [ ] The Art, Science, and Engineering of Fuzzing
• [ ] Boolean Satisfiability Solversand Their Applications inModel Checking
• [ ] Software Foundations - Logical Foundations
• [ ] Model Checking
• [ ] FORMAL METHODS IIT-D Lecture Slides
• [ ] Program Analysis, Verification & Testing Book
• [ ] The Science Of Programming
• [ ] Model Checking
• [ ] Building Secure Systems from Buggy Code with Information Flow Control
• [ ] Modular Verification of Secure Information Flow - Peter Müller
• [ ] CISSP Domain Security
• [ ] Delta Debugging
• [ ] What is fuzzing?
• [ ] AFL++

Some Methods & Basic Resources :

1. Induction is a way to prove things that are defined recursively.

• Base case, we show that either for 1 or 0 / starting cases some property is true.
• For some k th case we show that if we assume P(k) is true, P(k+1) is true
• From this we may conclude that P(n) holds for all n in our domain.

Introduction Videos :

Program Analysis & Verification

Fantastic videos by Dr. Subhajit Roy (IIT Kanpur)

• ACM School PAVT

Simple Inductions :

• https://www.youtube.com/watch?v=m_91KWQiC0o&list=PLA72M-qSGPm3Bnkc6iKGxrL1OARztbm6V

Tree Data Structure Induction :

• https://www.youtube.com/watch?v=Fy8cNMuk_rY&list=PLA72M-qSGPm3HZbcRLVOSpxELUHtdaNpt

Natural Deductions :

• https://www.youtube.com/watch?v=v2i59XRceXE&list=PLA72M-qSGPm2ohvwvJVbd3abnaSkiBy8j

2. Bounded Model Checking : We model the problem like a Finite State Machine. An execution of a FSM is a string formed by simulating the state-to-state transitions. We ask if a certain property holds for the FSM globally or eventually when we move from say State S1 to S2. The model is bounded in the sense that we consider a finite number of states but an have infinite number of executions or traces possible.

Turing Machine, As an extension to FSM :

• https://www.youtube.com/watch?v=QOcxbzopSk4&list=PLA72M-qSGPm27TjJaMOsNcMnLUoYAO9ZT

Model Checking :

• https://www.youtube.com/watch?v=piISG8bV2GI&list=PLJ5C_6qdAvBGojQMUzL4x5Y0N5gBJmT4l

How we model and define properties :

• https://www.youtube.com/watch?v=8wI5ee3Lwsw&list=PLJ5C_6qdAvBGojQMUzL4x5Y0N5gBJmT4l&index=13

LTL, this logic theory is needed to model temporal properties or state transitions where the property depends on time / or on the next state of execution. As in the case of an FSM, we need to check if property holds from state to state.

• https://www.youtube.com/watch?v=W5Q0DL9plns&list=PLJ5C_6qdAvBGojQMUzL4x5Y0N5gBJmT4l&index=33

For properties that need a set of set of traces to define and prove correctness, we need hyper-properties.

• https://www.youtube.com/watch?v=JZ5OWdX3hmY

Hoare Logic :

• https://www.youtube.com/watch?v=kjxdelbo9C4&list=PLA72M-qSGPm2bZlhxYB-ePerW0U8nPn4H
• http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/IncorrectnessLogic.pdf

Binary Search Verification in Dafny :

• https://www.youtube.com/watch?v=-_tx3lk7yn4

Dafny PDF :

• https://arxiv.org/pdf/1701.04481.pdf.

Calculus of Computation :

• https://link.springer.com/book/10.1007/978-3-540-74113-8

Hyperproperties :

• https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf.

Hedra Formal Methods :

• https://www.youtube.com/watch?v=6q15ytIOE3U

Detailed Study : For Research Orientated Learning

What is Computer Security ?

• https://www.microsoft.com/en-us/research/publication/practical-principles-for-computer-security/
• https://dl.acm.org/doi/pdf/10.1145/1592761.1592773

Propositional Natural Deductions :

• https://www.youtube.com/watch?v=v2i59XRceXE&list=PLA72M-qSGPm2ohvwvJVbd3abnaSkiBy8j

First Order Natural Deductions :

• https://www.youtube.com/watch?v=gggItiZ3Sjk&list=PLA72M-qSGPm1pISu85QR6bZL4wK4rZZxp

Hoare Logic Link :

• https://www.youtube.com/watch?v=t-Mj4ji3tCw&list=PLA72M-qSGPm2WxSxXthNiYx2u4KBZlXCC

Hoare Logic + Loops :

• https://www.youtube.com/watch?v=kjxdelbo9C4&list=PLA72M-qSGPm2bZlhxYB-ePerW0U8nPn4H

Induction :

• https://www.youtube.com/watch?v=m_91KWQiC0o&list=PLA72M-qSGPm3Bnkc6iKGxrL1OARztbm6V

Tree Induction :

• https://www.youtube.com/watch?v=Fy8cNMuk_rY&list=PLA72M-qSGPm3HZbcRLVOSpxELUHtdaNpt

Model Checking - 1 :

• https://www.youtube.com/watch?v=piISG8bV2GI&list=PLJ5C_6qdAvBGojQMUzL4x5Y0N5gBJmT4l

Model Chceking - 2 :

• https://www.youtube.com/watch?v=KrWSK-UzCRc&list=PLnbFC0ntxiqdpoWwMKCVh6BRwBePHaqQx

Linear Temporal Logic :

• https://www.youtube.com/watch?v=CUno7iGUmAo

Clause Learning (CDCL) :

• Clause learning : CDCL
• Handbook of SAT
• Conflict Driven Clause Learning - CDCL

Hyperproperties :

• https://www.youtube.com/watch?v=vVMu6g2H50Q

Verification Corner Dafny :

• https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A/videos

Verification Corner Loop Invariants :

• https://www.youtube.com/watch?v=spcfzbisBv4

UCLID5 :

• https://github.com/uclid-org/uclid/tree/master/tutorial
• https://cse.iitk.ac.in/users/spramod/papers/memocode18.pdf
• https://cse.iitk.ac.in/users/spramod/papers/ccs17.pdf

UCLID5 is based on Z3. Z3 Reference :

• https://theory.stanford.edu/~nikolaj/programmingz3.html
• https://z3prover.github.io/api/html/namespacez3.html
• https://github.com/Z3Prover/z3
• https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Dynamic Taint Analysis :

• https://users.ece.cmu.edu/~aavgerin/papers/Oakland10.pdf

The Calculus of Computation. (Bradley & Manna)

• Slides : https://lara.epfl.ch/w/_media/sav15:calculus-of-computation-slides.pdf

Non-Interference :

• http://csl.sri.com/papers/csl-92-2/csl-92-2.pdf

Hyperproperties :

• https://eprint.iacr.org/2019/310
• https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf
• https://arxiv.org/pdf/1905.13517.pdf

Probabilistic Symbolic Execution :

• Probabilistic Symbolic Execution
• PSE Paper

Probabilistic Programming :

• Hakaru

LLVM Frameworks :

• LLVM : Compilers Lab
• LLVM Ball-Laurus Profiler

Model Checkers :

• CBMC
• ESBMC

Concepts/Topics :

• Universal Quantification
• Uniqueness Quantification
• More on Hoare Logic
• Abstract Interpretation

Hands-On Stuff & Tutorials I made :

• Use of gcov & gtest
• Example use of gcov, gtest, cmake & make