Introduction into Formal Verification

Note: This course is not meant for believers. It's about to proof, that every fucking single keystroke, you're typing into your computer, is verifiable correct!

Disclaimer: If you feel offended, stop being offended!!!

Another warning: This is not a comfort zone for programmers, where you can endlessly load overly buggy, throughly backdoored libraries from dubious US sources and deliver to customers quickly!!!

Thank you for understanding!

The highest law in formal verification: "homoiconicity

"To understand language, you must have understood language!"

https://en.wikipedia.org/wiki/Homoiconicity

Note: Programming languages always are a subset of "the human language"

Here e.g. you can program in "human language": https://snap.berkeley.edu/snap/snap.html

Simply click on the gear ⚙ symbol left of "untitled" and change the labels of the programming tiles to your mother language!

Means: When you can easily implement your (programming-) language of choice in mainly your (programming-) language of choice very quickly, then - and only then - you can be sure, that all logical components of your (programming-) language are well thought through enough to build reliable, larger systems with it. You're allowed to bootstrap with a tiny part of **easily verifiable** assembler or machine code.

What hardware or operating system?

You must be able to remove all unused functionality in your system kernel and libraries from your machine. This only is possible, when:

a) Your operating system is built up in a modular way
b) You have full open access to all sourcecodes, even for the firmware within CPUs, controllers, and BIOS (UEFI)
c) Your operating system and libraries are tiny, "one human" readable and understandable
d) Your programming language compiler is small and verified itself
e) Your hardware and software have no backdoors
f) Your CPU contains no secret machine code instructions

Given all that, then there still is a huge risk, that the remaining functionalities in your kernel and libraries still have some undiscovered bugs inside!!!

Example: https://onecompiler.com/c/42kprej8s

1
2
3
4
5
6
7
8
9
#include <stdio.h>
int main()
{
    char name[50];
    printf("Enter name:");
    scanf("%s", name);
    printf("Hello %s \n" , name );
    return 0;  
}

Here the problem is the old POSIX function scanf that is still existing in Unix machines for downwards compatibility reasons.

!!! Fingers off CPUs without or deactivated MMU by UEFI !!!

Only CPUs with MMU can protect executable code from being overwritten by other processes. Here the C function https://man7.org/linux/man-pages/man2/mprotect.2.html is responsible for. On CPUs without MMU this function has no effect, is virtually disabled. Some Docker versions with Linux compiled as "User Mode Linux" Kernel - to be able to run in user space - have this disabled. Also some US influenced motherboard manufacturers silently disable MMU and IOMMU with unsigned (by NSA, Microsoft) Linux kernels, e.g. self compiled ones.

https://forum.proxmox.com/threads/iommu-not-activatable-uefi-systemd-boot.123776/

The alternative is the Harvard Architecture with its strict physical separation of Code and Data over two different busses.

Atomic Types and TOCTOU / TOCTTOU or TOC/TOU problems

C11, now standard in Linux, has <atomic types>. The GCC 14 Static Analyzer warns if there are <Race Conditions> or TOUTOU problems:

https://en.wikipedia.org/wiki/Race_condition
https://en.wikipedia.org/wiki/Time-of-check_to_time-of-use

https://mansky.lab.uic.edu/wp-content/uploads/sites/862/2022/07/conc-bst.pdf

Always consider Hyrum's law!!!

When YOU are responsible, that YOUR code is safe, then you have to go back to the root, the origins of all libraries existing.

Dependency

https://www.explainxkcd.com/wiki/index.php/2347:_Dependency

And that is the POSIX standard. This standard with its LEGO™ bricks gives you everything you need to fulfill your job.

Note: Only the POSIX mindset guaranties you portability of your software onto all operating systems available!

Sure, productivity can be higher with other languages and compilers and their mighty libraries that are coming with them. But be aware, that nothing of this stuff, created by millions of people across the world, is safe or under YOUR control.

The goal - expecially of US multinationals - is to pull you deeper and deeper into their swamp, making you finally totally dependent on that (functionally overloaded and thus highly insecure) stuff they have created:

https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=microsoft

Hyrum's law: https://www.hyrumslaw.com/

What programming language or compiler?

There is a huge difference in quality of compilers:

!!! Fingers off LLVM !!!

I think, this tells you everything: https://www.phoronix.com/news/LLVM-Record-Growth-2021

With its tens of millions of lines LLVM is much too large to be verified, everything is in heavy movement. How can it be of any use? And they are talking about the backend only!!!

Compare with Fabrice Bellard's tiny Intel 32 Bit C compiler - 2048 characters! Characters, not lines!!! Fabrice's compiler's and interpreters are "one human" understandable and maintainable. Only this guarantees long-term stability and safety.

Note: Don't use programming languages that rely on LLVM compiler backend. These people do not know, what they are doing, none of them!

Unluckily people do every nonsense for money! :-(

Even writing TypeScript parser for the TS to JS transpiler by hand! :-O

No grammar file, no parser generator, nowhere!!! ,:-(

Unlike Python 3.12:

https://github.com/python/cpython/blob/main/Grammar/python.gram
https://github.com/RobEin/ANTLR4-parser-for-Python-3.12/tree/main

Though there are people willing to help Microsoft: https://github.com/gcanti/parser-ts

Microsoft has already discovered parser generators, but obviously not using it for TS itself:

https://github.com/microsoft/ts-parsec

What about "safe" RUST with LLVM?

Rust obviously isn't almost as safe, as people claim: https://github.com/rust-lang/miri

Rust as language is as complex as C++ with its 2000 A4 pages language definition. So there is no chance to write a formal verification tool like the GCC Static Analyzer for C. Simply not doable, even if you had 100,000 man-years of capacity!!!

Howto emulate Rust Borrow Checker and Lifetimes in C?

Imagine a TODO list, where free CPUs can grab their (typically short, reentrant and idempotent) jobs from. On that TODO list a struct with three pointers: One pointer to the data (to be worked on), one with a pointer to the program and one pointer where the thread or process can put the result, e.g. the sorted list. This way the utilisation rate on Multi Core CPUs can be much higher. The other problem occurs, when closure variables disappear because the stack segment was deleted after e.g. a long jump machine code instruction. Here dangling pointers with "use after free" remain, a serious problem especially within JIT engines: https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=use+after+free

Fast interpreters with jump tables technology typically come very close to JIT engines, performance wise:

https://news.ycombinator.com/item?id=7947436

The excellent GCC compiler

It not only has an excellent formal verifier aka "GCC 14/Static Analyzer" onboard, it also supports a gazillion of architectures and combinations: https://tracker.debian.org/pkg/gcc-14

C programming language has a very bad reputation concerning security. But that has significantly changed now. You - seriously - should reconsider writing secure programs in C again, with GCC 14 Static Analyzer to verify your C-Code!!! It's an excellent teacher, finds every single bug now, making C the safest language on earth! (I know, plenty of people disagree here!!!)

Use of Variadic Macros with GCC Extensions

You may have noticed, that you can handover complete data streams from one GNU bash program to the other, like in the famous McIllroy word frequency count example:

https://franklinchen.com/blog/2011/12/08/revisiting-knuth-and-mcilroys-word-count-programs/

So the "arity" of function parameters or arguments in bash commands is endless: https://en.wikipedia.org/wiki/Arity

That, of course, must come from somewhere. How can i write functional style within C now?

Here's the solution: https://gcc.gnu.org/onlinedocs/cpp/Variadic-Macros.html

It's the base of all functional style programming with C!

CERT coordination center classified this functional style of programming as "high risk": https://en.wikipedia.org/wiki/Variadic_function

But luckily the GCC Static Analyzer takes out also that risk now.

What GCC Static Analyzer is able to find

https://github.com/davidmalcolm/gcc-analyzer-integration-tests

Output is in JSON, the SARIF standard: https://docs.oasis-open.org/sarif/sarif/v2.1.0/

(Btw.: Microsoft vs. i4i lawsuit: https://supreme.justia.com/cases/federal/us/564/91/)

Use parser generators and Finite State Machine compilers!!!

Writing parsers is very hard any maintaining them is even harder. Use Ragel, everywhere: https://www.colm.net/open-source/ragel/ From one, single grammar it generates code for many programming languages: https://github.com/topics/ragel

Note: Never, ever try to write your own parser. You get immediately lost in nested if ... then ... else if ... clauses and spaghetticode!!!

Second best alternative are State Machine Tables which use function pointers inside:

https://blog.mbedded.ninja/programming/general/control-methodology/a-function-pointer-based-state-machine/

Note, that in this special example the labels ST_LED_ON ... ST_IDLE are "pointer to function" each. In C you can e.g. write (*sin)(x) instead of sin(x) ... sin then is a pointer variable, pointing to the address in the C math library where the sine function can be found:

1
2
3
4
5
6
7
8
9
static stateTransMatrixRow_t stateTransMatrix[] = {
    // CURR STATE  // EVENT           // NEXT STATE
    { ST_INIT,     EV_ANY,               ST_IDLE    },
    { ST_IDLE,     EV_BUTTON_PUSHED,     ST_LED_ON  },
    { ST_LED_ON,   EV_TIME_OUT,          ST_LED_OFF },
    { ST_LED_ON,   EV_BUTTON_PUSHED,     ST_IDLE    },
    { ST_LED_OFF,  EV_TIME_OUT,          ST_LED_ON  },
    { ST_LED_OFF,  EV_BUTTON_PUSHED,     ST_IDLE    }
};

These State Tables are easily verifyable. They prevent you from writing endlessly nested if ... then ... else if ... clauses!!!

!!! Best exercise is to write your code without any "if" statement for a while!!!

Why not another IDE and no new verification language

There are a couple of proof systems:

TLA+: https://lamport.azurewebsites.net/tla/tla.html
TLA+ example: https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840.tla
TLA+ symbols: https://lamport.azurewebsites.net/tla/summary-standalone.pdf
TLA+ operators: https://learntla.com/core/operators.html
TLA+ excellent overview: https://members.loria.fr/SMerz/papers/tla+logic.pdf

Unluckily TLA+ has not become a mainstream proof system for the masses. That has to to with the problem of translation of propositional language into mathematical functions used in programming languages.

Computerphile: Propositions as Types:
https://youtube.com/watch?v=SknxggwRPzU

IDE for formal verification

Famous Leslie Lamport (LaTeX, CosmosDB) e.g. wrote such a tool - TLA+ - and even invented his own verification programming language to verify any algorithm within. But unluckily he never verified his verification tool! :-(

Same for all other languages and SAT solvers, verifiers, such as OCaml / COQ, Agda, Haskell, Idris, Idris2, Fstar, Z3, UML2CODE and CODE2UML converters e.g. for Smalltalk. None of them ever was verified if they could reliably verify.

All we have is a formally verified C compiler which does 100% bug free translation to machine code on certain CPUs. And we have an unverified GCC 14 Static Analyzer, which obviouls is doing an amazing job at the moment finding hundreds of thousands of bugs in the Linux kernel and other C written stuff, such as GTK4 libraries (GNOME Desktop).

What GCC Static Analyzer has tested

https://github.com/davidmalcolm/gcc-analyzer-integration-tests

This is an integration test suite for GCC's -fanalyzer option.

The idea is to build various C projects using a candidate installation of GCC with -fanalyzer, and capture the diagnostics in SARIF format.

apr-1.7.0
coreutils-9.1
Doom
git-2.39.0
haproxy-2.7.1
ImageMagick-7.1.0-57
Juliet-1.3 (a test suite for static analysis tools)
linux-5.10.162 (with allnoconfig)
pcre2-10.42
qemu-7.2.0
xz-5.4.0
zlib-1.2.13

Unluckily GCC Static Analyzer can't verify C++ stuff. C++ - apart from it is a highly complex programming language, which definition already is 2000 A4 pages long - it inserts things into the binary, that cannot be verified without having to verify the C++ compiler with its Template engine itself. E.g. abstract classes and virtual functions, coming with an internal garbage collector, which are themselves not coded in the C++ language Standard Libraries. They're deeply sticking in the C++ compiler binary itself.

Lisp e.g. is a surprisingly small language, once you have implemented and verified the λ calculus "engine": https://justine.lol/lambda/ The Lisp interpreter itself is implemented in λ calculus:

https://github.com/jart/sectorlisp/blob/main/lisp.lisp

This implementation of Lisp - its λ calculus is 512 bytes only - you can consider as "formally verified" and rock-safe

Also see this Lisp implementation in 99 LoC: https://github.com/Robert-van-Engelen/tinylisp

99linesLisp

Here a Lisp macro preprocessor for C: https://github.com/eratosthenesia/lispc

Lisp/C

Read the fucking manuals (RTFM)!!!

Of course, the bug in the scanf function is well known. For secure programming, always lookup the "quirks and features" in your Operating System handbook: https://man7.org/linux/man-pages/man3/scanf.3.html

Stackoverflow is no reliable source for anything. Especially not for our purpose. Use the programming man pages, that come installed by default with your machine, exclusively!

General philosophy in Unix about documentation

General philosophy within the Unix community is, that any undocumented feature or false description of a function is considered a bug!!!

Note: If your operating system has no such handbook on disk, it's competely unusable for our purpose!!!

What editor or programming tools?

Formal verification of code is hard stuff. You mainly "program" on paper to get things mentally right. Typing in more than one A4 page per day rarely happens. For secure programming you have to stay within one single programming language and compiler.

So you won't need any highly sophisticated editor or even IDE with e.g. lsp server to be able to fast switch through different programming languages and masses of mostly unknown, rarely security reviewed, always insecure libraries!!!

Note: Grabbing code from Github, NPM, Anaconda has to come to an end. No use of libraries without code review before!!!

Use literate programming, everywhere!

"Literate programming", invented by Donald E. Knuth (TeX), looks a bit like writing extensive tutorials with code snippets inside. You can use John Gruber's Markdown like i use for writing this tutorial here:

John Gruber's https://www.markdownguide.org/getting-started/ (he invented that stuff!)
Markdown library: http://demo.showdownjs.com/
Markdown server: https://python-markdown.github.io/

Live: Experienced programmer at work!

Watch Nir Lichtmann at work: https://youtube.com/watch?v=2HrYIl6GpYg

#include <sys/socket.h>
#include <string.h>
#include <fcntl.h>
#include <sys/sendfile.h>
#include <unistd.h>
#include <netinet/in.h>

void main() {
    int s = socket(AF_INET, SOCK_STREAM, 0);
    struct sockaddr_in addr = {
        AF_INET,
        0x901f,
        0
    };

    bind(s, &addr, sizeof(addr));

    listen(s, 10);

    int client_fd = accept(s, 0, 0);

    char buffer[256] = {0};
    recv(client_fd, buffer, 256, 0);

    // GET /file.html .....

    char* f = buffer + 5;
    *strchr(f, ' ') = 0;
    int opened_fd = open(f, O_RDONLY);
    sendfile(client_fd, opened_fd, 0, 256);
    close(opened_fd);
    close(client_fd);
    close(s);
}

He uses Vim or NeoVIM in a split window mode. One for editing code, one for looking up the Unix manuals.

Also see his other example, e.g. his minimalist chat server in 43 lines of C only!!!

Restricted Shells

Code in a way, that your programs only can run within a restricted shell:

https://www.gnu.org/software/bash/manual/html_node/The-Restricted-Shell.html

This simple shell can be the beginning of your own resticted containers: https://stevens.netmeister.org/631/apue-code/01/simple-shell.c

Warning: Docker is highly insecure!!! No kind of protection. None!

Are above examples safe code???

Yes! As you might have noticed, the above code only consists of declaritively lined-up statements.

Do i have to write Unit Tests? What kind of?

“Insanity is doing the same thing over and over and expecting different results.” That witticism - I'll call it “Einstein Insanity"!

So - nope! When you have formally verified your software, you don't need to do "tests" any longer. Safe is safe!

Keep in mind, that writing "safe software" firstly is a mental thing and secondly a question of self discipline and planful working!

What about fuzzing tests?

Fuzzing tests are used when the <state space> is too big to be fully searched through, e.g. when adding two 64 bit or multiplying two 32 bit integers. The range simply is too large to be fully searched. Apart from that an overflow can happen any time. That's what hackers are typically looking for their "buffer overflows".

Within formal verification you have to ***proof*** that your function cannot fail or output false results - under all circumstances!!!

YOU have to proof, that you have already seached through the full <state space> and that no input of any kind can harm your function. So <fuzzing> is pretty useless then! It only would be a subset of <state space> you have already searched through!

The formal verification mindset

Note: It is overly important that you start to think in categories of <state space> that has to be completely searched through and concetensted transformers which <precondition> and <postcondition> in each of them.

Thinking in <state spaces> and <transformers>

tr -cs A-Za-z '\n' | tr A-Z a-z | sort | uniq -c | sort -rn | sed ${1}q

Totally avoid <shard state> between functions. No overlap, never ever! Otherwise your programs are not verifyable. Or the GCC14 Static Analyzer explodes. Do <pure functions> only. Use <pure functions> as transformers. In the above example no state is shared between tr, sort, uniq and sed. Only do verifyable steps, one after the other. Document them in literate programming, like in this http://rentry.co/how Markdown engine here.

Split up your functions into small, reentrant, idempotent pieces

/* Write your code reentrant, use closures! */
/* Use declarative style, everywhere */
/* Use idempotency, everywhere! - otherwise no threadsafe! */
/* Use actor style, eveywhere ! */
/* Use Fowler's Inversion-of-Control pattern */
/* Split your code up into microtasks */
/* Fire up a nested virtual machine for each microtask, only for seconds*/
/* Dont give hackers time to upload their code (!!!) */
/* Alternatively use fork() and throw away the stack, heap */
/* Use Linux KSM features */
/* Use Linux RealTime OS (RTOS) features */

void foo() {
    static int x = 5; // assigns value of 5 only once
    x++;
    printf("%d\n", x);
}

int main() {
    foo(); // x = 6
    foo(); // x = 7
    foo(); // x = 8
    foo(); // x = 9
    return 0;
}

/* You got the idea(s)! */

https://onecompiler.com/c/42kytdugf

Note: Never leave this programming pattern shown here!!! Otherwise you find yourself soon in real, deep trouble! (at minimum jobless)

The thinking in <state space> school

What's wrong with this example?

int a := int b + int c;

It may pass ***your*** unity tests, but hackers always bring functions to its limits, always looking for unintended or unexpected <side functionalities> suddenly operning up. The problem here: You suddenly have 33 bits or 65 bits. So you have to make sure you verify and limit your inputs that no harm can happen.

Even double worse: int x := int x * int a; (When you write that, you're fired !!!)

You have to do and document that for every fucking function and system call you use!!!

!!!!! YOU have to verify every fucking statement, with no exception !!!!!!

Use languages with sound types and proven algorithms only!

Only use proven algorithms and implementations.

Use interpreters and programming language implementations with sound types only!!! E.g. Dart 2.1, QuickJS, GNU Smalltalk, eLisp

https://dart.dev/language/type-system
https://bellard.org/quickjs/ (has BigNum, ...)
https://www.gnu.org/software/gcl/
https://www.gnu.org/software/smalltalk/manual-base/html_node/Fraction.html
https://www.gnu.org/software/smalltalk/manual-base/html_node/ScaledDecimal.html
Only exception: C in combination with the GCC 14 Static Analyzer!

(print (expt 256 256))

Result:
32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448283120630877367300996091750197750389652106796057638384067568276792218642619756161838094338476170470581645852036305042887575891541065808607552399123930385521914333389668342420684974786564569494856176035326322058077805659331026192708460314150258592864177116725943603718461857357598351152301645904403697613233287231227125684710820209725157101726931323469678542580656697935045997268352998638215525166389437335543602135433229604645318478604952148193555853611059596230656

https://onecompiler.com/commonlisp/42kyvcye3

GNU Smalltalk sound types: http://tpcg.io/_JZSTQ1

If your interpreter or compiler is not able to do that easily, the amount of things, you have to check and proof "undangerous" - explodes!

Remember: "YOU have to proof, that your program IS safe!!!"

Example for failed algorithm: Timsort

https://www.cwi.nl/en/news/java-bug-fixed-formal-methods-cwi/

Reminder: You are responsible for use of libraries, nobody else!!!!

Playing around with state space ...

Question to popcount: How man possibilities do i have to spread 4 bits in one byte?

https://www.calculatorsoup.com/calculators/discretemathematics/combinations.php

70^(8 Byte, 64 bits) = 576.480.100.000.000 = 576 Billionen (engl. "trillion")

(print (expt 70 8)) -> https://onecompiler.com/commonlisp/42kyyxgy7

POPCOUNT in Broadcom Tomahawk chip: https://github.com/opennetworkinglab/SDKLT

https://www.broadcom.com/products/ethernet-connectivity/switching/strataxgs/bcm78900-series

https://github.com/Kleidukos/popcount-benchmark
https://github.com/BartMassey/popcount

Compare with other trees: https://github.com/runshenzhu/palmtree

Dr. Askitis' hash benchmarks: https://github.com/Tessil/hat-trie

https://youtube.com/watch?v=DMQ_HcNSOAI&t=1860s

https://github.com/strager/perfect-hash-tables

General security problem with high performance tuned code

https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=Image
https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=Video
https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=Animated
https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=Streaming
https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=Font

Put your f***ing fingers off streaming, video, graphics and image animation libraries!!!

!!!! I mean that, seriously!!!! No compromises!!!!!

No compromises for critical infrastructure in your organisation

If someone forces you to do that, immediately quit your job !!!

Ziprecruiter is your friend!!

End of discussion

A simple Hoare Semantic Triple proof system in Python

https://daltron.de/posts/hoare-prover/ (based on Z3)

Your just invented algorithm you want to proof:

1
2
3
4
5
6
[x, y, z, A, B]
{x==A and y==B}
z := x;
x := y;
y := z;
{x==B and y==A}

The core idea: Concatenated transformers like in formal programming languages or in this famous bash example from Donald E. Knuth and Doug McIlroy:

$ tr -cs A-Za-z '\n' | tr A-Z a-z | sort | uniq -c | sort -rn | sed ${1}q

1
2
3
        {P}C₁{R} {R}C₂{S} {S}C₃{T} {T}C₄{Q}   
_______________________________________________   (transforms into:)
               {𝑃}𝐶₁C₂C₃C₄{Q}

His original comment on Knuth's solution: "Knuth has shown us here how to program intelligibly, but not wisely. I buy the discipline. I do not buy the result. He has fashioned a sort of industrial-strength Fabergé egg—intricate, wonderfully worked, refined beyond all ordinary desires, a museum piece from the start."

https://franklinchen.com/blog/2011/12/08/revisiting-knuth-and-mcilroys-word-count-programs/

Note: Without knowing Hoare Triple and Computer Science Notation no job in german security industry!

https://web.archive.org/web/20240717214829/https://wwwmayr.in.tum.de/konferenzen/Jass08/courses/2/lang/paper_lang.pdf
https://moves.rwth-aachen.de/wp-content/uploads/SS19/savos/exercises/ex-07.pdf

Note: Learn Computer Science Meta-Notation!

Guy Steele about CSM: https://youtube.com/watch?v=7HKbjYqqPPQ

Two of the most influencing people in Computer Science. Rich Hikey and Guy Steele:
https://youtube.com/watch?v=dCuZkaaou0Q

Fractal and Hitchhiker Trees (immutable data structures on disk): https://youtube.com/watch?v=jdn617M3-P4

Note: Watch these videos! They're highly important for security and the future of programming!!!

Back to: https://rentry.co/DSRsecuritycoursepart0

And then let's switch over to learn some math: https://rentry.co/DSRsecuritycoursepart13

Edit
Pub: 22 Jul 2024 14:38 UTC
Edit: 25 Jul 2024 12:56 UTC
Views: 282