DSR enhanced security and "formal verification" course
Note: First parts of this course are an overview of security related problems. Later we refine, are "zooming into" the details.
- The Chrome Browser nightmare
- The secret source that made Amazon #1 in the world - The "Stuffer Concept"
- Is Rust a safe language?
- The F* formally verified language that transpiles to OCaml and C
- The GCC 14 static analyzer
- BOLT - The binary code optimizer
- The Google Closure Compiler for JavaScript
- TCC - the alternative to the big players:
- CompCert - the formally verified C compiler
- What are in-memory file descriptors - memfds?
- Seccomp, eBPF, and the Importance of Kernel System Call Filtering
- Pledge, the perhaps most sophisticated sandbox for Linux
The Chrome Browser nightmare
https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=use+after+free
Let's discuss the impact on Desktop Computers:
- What problems do firewalls generally do not solve?
- any idea?
- What problems firewalls can solve?
- other ideas?
Firewalls are primitive things. On IP level (see the ISO/OSI model) they prevent that you can initiate a connection from outside the intranet. They're doing it over keeping record, track over the SYN/ACK-ACK handshake. Most of them do not filter contents since they are unable to intercept HTTPS traffic. And even if they are, they only recognize the most relevant "hot" virus/trojan signatures from the publically maintained OWASP archive. Individual, "hand written" attacks they generally can't recognize. Sometimes even old viruses pass again and even newer, recent ones with old encodings, such as UUCP in Mail attachments, are overseen.
The secret source that made Amazon #1 in the world - The "Stuffer Concept"
Not only kernel malloc()'s are costy in terms of clock cycles. There comes an inherent security risk of all kinds of stack/heap overflows, "use after free" (see above), "code injection" and other exploiting methods with it. Google and Amazon AWS therefore were working on their own collection of user space allocators, "garbage collectors", e.g. in Google's "gVisor" wrapper / secure container solution, see: https://gvisor.dev/
The perhaps most sophisticated, "secure" memory system is:
"The stuffer concept": https://youtube.com/watch?v=yY0A3Zmeiv0&t=38m30s
It is used in Amazon's TLS library, which is the most exposed library at all, since you typically connect to potentially hostile servers or clients in the early pre-authentication phase, before the encrypted and authenticated HTTPS transfer starts. Also see the problematic DHKE with its possible "MITM attack" for e.g. TLS 1.2 which is the most used algorithm as of today.
Here the short introduction into their ideas: https://github.com/aws/s2n-tls
The final Stuffer Code: https://github.com/aws/s2n-tls/tree/main/stuffer
Is Rust a safe language?
https://www.google.com/search?q=rust+%22-release%22+turn+off+bounds+check
https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=rust
https://readyset.io/blog/bounds-checks
https://foundation.rust-lang.org/news/unsafe-rust-in-the-wild-notes-on-the-current-state-of-unsafe-rust/
"How much rust code is actually safe?" https://youtube.com/watch?v=z_RekEdKcfk
"Bugs found by Miri": https://github.com/rust-lang/miri
While GCC compiler backend has quite matured and is reaching almost perfection with its GCC 14 "Static Analyzer" - which by the way - is for the C language (not C++ or other languages) only, LLVM seems to be a pure mess:
When it comes to code churn, LLVM in 2021 saw 12.5 mllion lines of code added and 8.3 million lines removed... https://www.phoronix.com/news/LLVM-Record-Growth-2021 - WTF!
Compare that to that incredibly small Plan9 C compiler code base, recently ported to RISC-V: https://youtube.com/watch?v=LHJqdXGb0uc
The following is a table of the source size of the Plan9 C compiler.
How can such a giant LLVM code base ever be "formally verified" like in http://CompCert.org ?
The F* formally verified language that transpiles to OCaml and C
https://fstar-lang.org/ (Note that here again french INRIA is involved!!!)
https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf
https://fstarlang.github.io/lowstar/html/
https://web.archive.org/web/20210104190243/https://www.fstar-lang.org/tutorial/
The GCC 14 static analyzer
BOLT - The binary code optimizer
The Google Closure Compiler for JavaScript
The smalltest bricks you can split your source code into are "Closures". After the extensive flow analysis you can recompose your code and not it will be smaller, but also much faster. VSC wouldn't run at all without that optimization:
https://github.com/google/closure-compiler
Closures e.g. allow to define a local variable or - especially in functional languages - even a new function inside a called function. That variable then is remembered when you come back. Closures are "reentrant". Webservers can recognize you over the Unique UUID burnt into your browser even when coockies are deactivated or deleted.
TCC - the alternative to the big players:
Also see TCC and it predecessor, the OTCC - see: https://bellard.org/tcc/ and https://bellard.org/otcc/
Looking into TCC code generation: https://briancallahan.net/blog/20220406.html
Combine with GCC Static Analyzer!
CompCert - the formally verified C compiler
How they're doing it, basically? When the generated binary code can be back translated to C, and both are identical, then it's "verified". VC++, LLVM, Emscripten are known to insert nasty things, same as Microsoft VSC is revealing to it's "master" what you are working on.
https://compcert.org/compcert-C.html
What are in-memory file descriptors - memfds?
How a attack works: https://magisterquis.github.io/2018/03/31/in-memory-only-elf-execution.html
The recorded live attack: https://asciinema.org/a/173715
Background to prevent those attacks: https://lwn.net/Articles/851813/
Seccomp, eBPF, and the Importance of Kernel System Call Filtering
https://dzone.com/articles/seccomp-ebpf-and-the-importance-of-kernel-system-c
Pledge, the perhaps most sophisticated sandbox for Linux
Made by Google employee Justine Tunney: https://justine.lol/pledge/
Pledge's predecessor, the $chroot command and *chroot() function:*
The bash command: https://man7.org/linux/man-pages/man1/chroot.1.html
The C function: https://www.man7.org/linux/man-pages/man2/chroot.2.html
A self made Restricted Shell: https://stevens.netmeister.org/631/apue-code/01/simple-shell.c
Howto break it: http://www.unixwiz.net/techtips/mirror/chroot-break.html
Alternatives:
Google's gVisor, the most secure free solution on the market: https://gvisor.dev/
Outdated: SECCOMPnurse, funded by the European Commission: https://www.chdir.org/~nico/seccomp-nurse/
Have fun!
Back to: https://rentry.co/DSRsecuritycoursepart1 Up to next lesson - https://rentry.co/DSRsecuritycoursepart3