Unix forever!

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

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.

1
2
3
4
5
6
7
8
lines   module
 509    machine-independent headers
1070    machine-independent YACC source
6090    machine-independent C source
 545    machine-dependent headers
6532    machine-dependent C source
 298    loader headers
5215    loader C source

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

https://developers.redhat.com/articles/2024/04/03/improvements-static-analysis-gcc-14-compiler#solving_the_halting_problem_

BOLT - The binary code optimizer

https://research.facebook.com/publications/bolt-a-practical-binary-optimizer-for-data-centers-and-beyond/

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

Edit
Pub: 26 Jun 2024 15:14 UTC
Edit: 28 Jul 2024 19:10 UTC
Views: 16440