The motivation: https://rentry.co/DSRsecuritycourseMotivations
DSR enhanced security and "formal verification" course
First parts of this course are an overview of security related problems. Later we refine, zoom into the details.
KISS principle: Markdown used in this course
Markdown tutorial: https://rentry.co/how
See course code: https://rentry.co/DSRsecuritycourse/edit
Mark Gruber's Markdown: https://showdownjs.com/
Live Markdown demo: https://markdownlivepreview.com/
How RegExp convert Markdown into HTML
See: https://medium.com/@mattkenefick/regular-expressions-markdown-to-html-anchors-1e7d52905517
- Example security problem(s)
- Intel Firmware: The total security meltdown
- Linus Torvalds: RISC-V Repeating the Mistakes of Its Predecessors
- OWASP TOP 10 attacks
- The x86-64 stack frame layout
- Snort - the Network Intrusion Detector
- One problem seems to be - buggy parsers
- Fast forward >> - Writing perfect parsers
- The mother of all parsers: The Finite State Machine (FSM)
- Perfect documentation:
- Parsing programming languages
- Masterpiece Petitparser
- Masterpiece Ragel parser
- Masterpiece Lemon Parser Generator
- Masterpiece OMeta / Ohm parser
- The old ANTLR Java eBNF parser
- Even CPython now uses grammar definition to parse the syntax tree!
- Emacs parser generator in Lisp
- Nim programming language parser generator
- Other solutions from Google
- Why is C considered a "dangerous" programming language?
- Can PVS-Studio C++ Analyzer help here?
- GCC Static Analyzer for C to the rescue
- Well done C program examples
- How complex is Assembler?
- General problem: Multithreading, Multicore and Synchronization
- The Binary Standard CDECL
- The biggest money grave: Language bindings
- The secure Eiffel programming language {P} C {P}
- Are Unit Tests enough? What is Fuzzing doing? TLA+? Agda?
- How complex a compiler has to be? Fabrice Bellard's OTCC Compiler
- How fast a webserver can be?
- What languages do runtime range and bound checkings?
- Programming Languages transpiling to C as Intermediate Language
- Webassembly as solution?
Example security problem(s)
Remote Code Execution attacks: https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=Microsoft+remote
The worst security bug ever: https://msrc.microsoft.com/update-guide/vulnerability/CVE-2024-30078 ; https://youtube.com/watch?v=I3tLkTdRvI0
Exchange Server - the never ending story: https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=%22Microsoft%20Exchange%20Server%22
Outlook attackable through firewall: https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=%22Microsoft%20Outlook%22
Microsoft Defender: https://www.exploit-db.com/exploits/51960
Fishbowl.c attack: https://gist.github.com/rain-1/be98648b0172817ec1c90d46942793bd
Who the fuck is Pascal Michaud? https://www.cvedetails.com/vulnerability-list/vendor_id-1341/Pascal-Michaud.html
SoftIce Debugger for Windows 11 - GNU licensed: https://github.com/vitoplantamura/BugChecker
The perhaps most sophisticated visual disassembler: https://github.com/NationalSecurityAgency/ghidra
Intel Firmware: The total security meltdown
UEFI ring -2 vulnerability. This is the worst thing that could ever happen!
What happens if there's a vulnerablility in your motherboard? Today we dive deep on a UEFI vulnerability that allows for a user to run code at... Ring -2: https://youtube.com/watch?v=rsd-LwCyY4s
INTEL® Management Engine: This is the biggest backdoor ever!
How to Hack a Turned-Off Computer, or Running Unsigned Code in Intel Management Engine: https://youtube.com/watch?v=9fhNokIgBMU
In our presentation, we will tell how we detected and exploited the vulnerability (explained in this Briefing: • Intel ME: Flash File System: https://youtube.com/watch?v=mYsTBPqbya8 ), and bypassed built-in protection mechanisms.
By Maxim Goryachy & Mark Ermolov
Behind the Scenes of Intel Security and Manageability Engine:
https://youtube.com/watch?v=TsXzDFjXj2s
Running within each Intel CPU since 2008: MINIX-3 https://www.minix3.org/
https://www.zdnet.com/article/minix-intels-hidden-in-chip-operating-system/
Linus Torvalds: RISC-V Repeating the Mistakes of Its Predecessors
Recent Torvalds interview: https://youtube.com/watch?v=1Y82U450zcI
What did he mean?
A Security RISC? The State of Microarchitectural Attacks on RISC-V
By Lukas Gerlach , Michael Schwarz , Daniel Weber from TUM:
https://youtube.com/watch?v=HCZ6DCu2ciE
Reproducing this new (end 2023) speculative execution attack
What do you need to execute this attack? C, Intel assembler knowledge, an unpatched C compiler, Vi, hex editor
Further ingredients: Paul Kocher, Intel VTune papers
- A high end Intel Server CPU (does not work on AMD EPYC!)
- Paul Kocher papers: https://ieeexplore.ieee.org/ielx7/8826229/8835208/08835233.pdf
- ??? https://www.paulkocher.com/doc/MicrosoftCompilerSpectreMitigation.html ???
- More Paul Kocher papers: https://dl.acm.org/doi/10.1145/3399742
- https://github.com/winter2020/oo7/blob/master/README.md
- https://www.comp.nus.edu.sg/~abhik/pdf/TSE20_oo7.pdf
- https://www.google.com/search?q=intel+profiling+assembler+instructions
- Install Valgrind and Cachegrind
- Find those Intel profiling machine code instructions to read out the "historic cache buffer": https://kernel-recipes.org/en/2018/live-blog-day-3-1/
- Put your performance engineer hat on! Good luck!
Follow Thomas Gleixner from german: https://www.linutronix.de/company/team.php on linux kernel mailing list.
Unlike former Spectre attacks, where information from protected memory pages only were dripping out, with using the Intel VTune profiler machine code instructions it is possible to read out megabytes of data per second: Credentials, password hashes ... combine e.g. with Mimikatz and Hashcat:
Worlds nicest Windows credentials grabber:
https://github.com/gentilkiwi/mimikatz
"World's fastest and most advanced password recovery utility"
https://github.com/hashcat/hashcat
Do address randomization, kernel and compiler patches mitigate?
No! That's like swimming in the sea with an umbrella for not to get wet:
The problem: (replace Nebraska by Seattle legacy code)
What's Google's workaround?
Google has split up all their code e.g. their Spanner / BigTable / F1 database into reentrant, idempotent functions only being active for a few seconds. With new nested virtualization you can do that almost without no overhead:
What's Amazon's workaround?
Better protection against buffer heap overflows, they've modified or replaced malloc() by something they call "stuffer concept". Instead of fopen(), fseek(), fwrite(), fclose() they use a append-only, blockchain like (and thus easy replicatable, backupable) single file storage engine, separating storage and compute:
https://github.com/neondatabase/neon
https://github.com/orioledb/orioledb
https://www.sqlite.org/onefile.html
"The stuffer concept": https://youtube.com/watch?v=yY0A3Zmeiv0&t=38m30s
Sources: https://github.com/aws/s2n-tls
Stuffer Code: https://github.com/aws/s2n-tls/tree/main/stuffer
How is Microsoft Azure mitigating that?
They're unable to throw out hackers from Azure: https://www.google.com/search?q=microsoft+ceo+brad+smith+grilled
Installation of Windows 10 and 11 demand an Azure account: https://www.zdnet.com/article/windows-setup-which-user-account-type-should-you-choose/
Next problem: Firing up a Linux Container within Azure takes a whole minute! -> Google concept does not work here!
Allowing C# and .NET only within a container has two major disadvantages: .NET JIT compiles at startup and needs time for "warmup phase" (see the Self compiler "hotspot concept").
The ongoing hacker attacks on Azure produce phantasy bills for thousands of customers.
Compare with C written: https://www.fossil-scm.org/home/doc/trunk/www/index.wiki
Bottom line: This page was generated in about 0.008s by Fossil 2.25 [cd50820410] 2024-07-04 00:05:41
OWASP TOP 10 attacks
Nice try to divert attention from above problems: https://owasp.org/www-project-top-ten/
The x86-64 stack frame layout
Example: https://owasp.org/www-community/attacks/Buffer_overflow_attack
https://eli.thegreenplace.net/2011/09/06/stack-frame-layout-on-x86-64/
Snort - the Network Intrusion Detector
Snort uses OWASP signatures to sniff on networks.
https://www.snort.org/
https://www.snort.org/rules_explanation
https://www.linkedin.com/pulse/sniffing-out-bad-guys-unveiling-snort-network-security-nimnas-ahamed-gkaec
One problem seems to be - buggy parsers
Worst example is Microsoft TypeScript: https://github.com/microsoft/TypeScript/blob/main/src/compiler/parser.ts
What is "Return Oriented Programming"? https://en.wikipedia.org/wiki/Return-oriented_programming
Howto do "Return Oriented Programming": https://book.hacktricks.xyz/binary-exploitation/stack-overflow , https://tripoloski1337.github.io/ctf/2020/01/26/return-to-libc-attack.html
The AWS "Return Oriented Programming" course: https://training.hacktricks.xyz/courses/arte
The Hacker Exploits Database: http://exploit-db.com
Windows 11 Zero-Day Exploit: https://www.exploit-db.com/exploits/51574
Windows 11 remote code Outlook attack: https://github.com/nu11secur1ty/Windows11Exploits/tree/main/2023/CVE-2023-33131
Fast forward >> - Writing perfect parsers
ANTLR eBNF grammar collection: https://github.com/antlr/grammars-v4
ES5 & ES6 parser: https://github.com/ohmjs/ohm/tree/main/examples/ecmascript
Fearless PEG parsing: https://dubroy.com/blog/visualizing-packrat-parsing/
MySQL parser in Goyacc: https://www.dolthub.com/blog/2023-07-28-goyacc-parser-tips-tricks/
TiDB SQL parsing: https://github.com/pingcap/tidb/blob/master/pkg/parser/parser.y
OMeta parser generator: http://www.tinlizzie.org/ometa/
OHM parser generator: https://ohmjs.org/pubs/live2016/
The idea for OHM goes back to an old paper by Philip Wadler, Erik Meijer and Graham Hutton: https://www.cs.nott.ac.uk/~pszgmh/monparsing.pdf
Watch Graham Hutton's famous YouTube Video howto use Parser Combinators: https://youtube.com/watch?v=dDtZLm7HIJs
The mother of all parsers: The Finite State Machine (FSM)
https://github.com/gbmhunter/FunctionPointerStateMachineExample/
The problem in TLA+: https://www.learntla.com/topics/state-machines.html
Use Graphviz for visualization: https://graphviz.org/Gallery/directed/fsm.html
https://sfriederichs.github.io/how-to/graphviz/2017/12/07/State-Diagrams.html
Python State Table Diagram generation: https://github.com/ckarageorgkaneen/sttp
Theoretical into into State Machines: https://spesml.github.io/plugin/state_machines.html
Learning Computer Science Meta - Notation (CSM): https://cs.stackexchange.com/questions/83770/help-understand-the-notation
Slides from Cambridge: http://www.cl.cam.ac.uk/teaching/1718/Semantics/slides.pdf
Perfect documentation:
Linux as zoomable graph
https://makelinux.github.io/kernel/map/
Can you please show me the Windows Server kernel map?
The famous SQLite Railroad Syntax Diagrams
https://www.sqlite.org/syntaxdiagrams.html
https://www.sqlite.org/th3.html
Nice diagrams automatically generated from Lemon Parser Generator: https://sqlite.org/src/doc/trunk/doc/lemon.html
Can Code Dependency Graphs help?
Kachegrind: https://kcachegrind.sourceforge.net/html/Home.html
https://www.google.com/search?q=gcc+call+graph+export+graphviz
https://en.wikipedia.org/wiki/Dependency_graph
https://en.wikipedia.org/wiki/Call_graph
https://understandlegacycode.com/blog/safely-restructure-codebase-with-dependency-graphs/
Microsoft's: https://www.ndepend.com/
Parsing programming languages
Masterpiece Petitparser
https://www.google.com/search?q=petitparser+grammar
"Let's eat, grandpa!": https://blogs.illinois.edu/view/25/475082
Petitparser is used by:
https://scg.unibe.ch/research/petitcompiler
https://stefan-marr.de/
https://stefan-marr.de/2020/12/shape-of-large-source-code/
https://moosetechnology.org/
http://agilevisualization.com/
Github: https://petitparser.github.io/
Petitparser for Dart: https://pub.dev/packages/petitparser
Petitparser for Java: https://github.com/petitparser/java-petitparser
Petitparser for Python: https://pypi.org/project/petitparser/
Petitparser documentation: https://pub.dev/documentation/petitparser/latest/
Masterpiece Ragel parser
Ragel homepage: https://www.colm.net/open-source/ragel/
Ragel Cheatsheet: https://github.com/calio/ragel-cheat-sheet
ehttpd - the 20KB ESP32 webserver: https://github.com/DavidPu/ehttpd
Page 47 - Code generation for C, C++, C#, Go, Java, Ruby: https://www.colm.net/files/ragel/ragel-guide-6.10.pdf
Looking into a simple Ragel C Mail - Parser:
https://github.com/adrian-thurston/ragel/blob/master/examples/mailbox.rl
Compare: https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=Outlook+remote+code
Ragel projects on Github: https://github.com/topics/ragel
Bonus: "Clang" parser written in 119 LoC Ragel: https://github.com/adrian-thurston/ragel/blob/master/examples/clang.rl
Markdown Ragel: http://rwx.io/posts/parsing-a-simple-markdown-stle-list-in-ragel/
Ragel and Go: https://ekhabarov.com/post/ragel-state-machine-compiler/
Masterpiece Lemon Parser Generator
Used by rock solid SQLite aka IndexedDB:
https://sqlite.org/src/doc/trunk/doc/lemon.html
Ambiguity: "Let's eat, grandpa!" vs. "Let's eat grandpa!" (commas safe lifes!)
"Ambiguity" in Lemon: https://sqlite.org/src/doc/trunk/doc/lemon.html#precrules
Masterpiece OMeta / Ohm parser
https://tinlizzie.org/ometa-js/#Lambda_Calculus
https://ohmjs.org/editor/
https://github.com/ohmjs/ohm/
https://github.com/ohmjs/ohm/tree/main/examples
The old ANTLR Java eBNF parser
The reason why Intellij IDEA, PhpStorm, PyCharm ... are all written in Java
The ANTLR4 parser: https://github.com/antlr/antlr4
ANTLR4 grammars: https://github.com/antlr/grammars-v4
https://texteditors.org/cgi-bin/wiki.pl/wiki.pl?JavaBasedEditors
ANTLR was the reason why Microsoft created the LSP server protocol:
https://github.com/microsoft/language-server-protocol
Even CPython now uses grammar definition to parse the syntax tree!
https://github.com/python/cpython/blob/main/Grammar/python.gram
Emacs parser generator in Lisp
This project is also about implementing algorithms described in the book The Theory of Parsing, Translation and Compiling (Volume 1) by Alfred V. Aho and Jeffrey D. Ullman (1972). Additional this project is about me learning how to parse programming languages.
At the moment it is possible to generate canonical LR(k) parsers using this library for complex languages like PHP 8.1.
https://github.com/cjohansson/emacs-parser-generator
eLisp is certified by the US FAA for use within aircrafts!!!
https://www.faa.gov/aircraft/air_cert/step/disciplines/aircraft_computer_software
Freight lists, globally, are operated with TCL a "infix" Lisp like language:
Used by: https://www.safe.com/company/
Karl Lehenbauer, "TCL: The Tool Command Language - LISP for the Masses"
https://youtube.com/watch?v=3YwFHPFL20c
https://support.safe.com/hc/en-us/articles/25407779413261-Startup-and-Shutdown-TCL-Script-Examples
TCL/TK under the name "Tkinter" comes preinstalled with every Python installer as standard library for GUI:
https://docs.python.org/3/library/tkinter.html
https://github.com/python/cpython/blob/3.12/Lib/tkinter/ttk.py
https://wiki.tcl-lang.org/page/List+of+ttk+Themes
Password Quicksafe: https://github.com/p-e-w/quicksafe
Nim programming language parser generator
Note: Nim is a high level language that directly transpiles to C or JS!
Introducing Synthesis: a Finite State Machine generator
https://forum.nim-lang.org/t/5688
https://github.com/mratsim/Synthesis#displaying-the-state-machine
Verify the generated, final C code with GCC Static Analyzer!
Other solutions from Google
https://www.google.com/search?q=nested+if+then+else+finite+state+machine+generator
#1: https://www.tu-ilmenau.de/fileadmin/Bereiche/IA/sse/Pubilcations/2004/IWK2004_fsm_code_synthesis.pdf
#2: https://beta.boost.org/doc/libs/1_31_0/libs/mpl/doc/paper/html/example.html
Note: No implementation of any kind of control flow without either State Machine Transition Tables or grammar definitions. Never, ever!!!!
In general: Keep away from software that contains longer nested if-then-else structures. These people are not knowing what they are doing!
Why is C considered a "dangerous" programming language?
Note: It isn't!! You only have to use State Machine compilers / generators like Lemon or Ragel: https://www.colm.net/open-source/ragel/ Output is rock-solid, always bug free!
Use: https://developers.redhat.com/articles/2024/04/03/improvements-static-analysis-gcc-14-compiler
https://readwrite.com/the-nsa-list-of-memory-safe-programming-languages-has-been-updated/
The NSA full report: https://www.nsa.gov/Press-Room/News-Highlights/Article/Article/3215760/nsa-releases-guidance-on-how-to-protect-against-software-memory-safety-issues/
https://www.techrepublic.com/article/white-house-report-memory-safe-programming-languages/
Considered "secure":
- Go
- Rust
- C#
- Swift
- Java
- Ruby
- Python
- Delphi/Object Pascal https://stackoverflow.com/questions/4083356/array-begin-from-0-or-1-in-delphi-5-0-pascal (Pascal strings: First element is length, so it's a 1-indexed language)
- Ada
Bad Example: abs(-2147483648) < 0 From: https://www.fefe.de/intof.html
Simple Bit Operations Tutorial: https://en.wikipedia.org/wiki/Bitwise_operation
Advanced "Bit Twiddling Hacks" - great programmer stuff: https://graphics.stanford.edu/~seander/bithacks.html
The problem: Windows is written in C++, Linux and GTK/GNOME are written in C!
Can PVS-Studio C++ Analyzer help here?
https://pvs-studio.com/en/pvs-studio/
GCC Static Analyzer for C to the rescue
https://developers.redhat.com/articles/2024/04/03/improvements-static-analysis-gcc-14-compiler
https://gcc.gnu.org/wiki/StaticAnalyzer
Reminder: Evil C-Pointers: https://www.thegeekstuff.com/2011/12/c-pointers-fundamentals/
Quick introduction into C: https://user-web.icecube.wisc.edu/~dglo/c_class/index.html
Dr. Chuck Severance excellent C and Python courses:
Code: https://github.com/csev and 18 hours of C training: https://youtube.com/watch?v=PaPN51Mm5qQ
Well done C program examples
Microsoft (accidentally?) sabotaged Mongrel Github repository: https://github.com/mongrel2/mongrel2/tree/master/src
https://lab.abilian.com/Projects/Cython+/Web%20server/Mongrel2/
Why Mongrel2? It's using Ragel parser to generate rock solid code:
https://github.com/lxu4net/RagelHttpParser/blob/master/ragel/http11_parser.rl
https://www.gnu.org/software/libmicrohttpd/
SQLite is using the Lemon Parser Generator: https://sqlite.org/src/doc/trunk/doc/lemon.html
Also see: https://www.sovereigntechfund.de/de/tech/libmicrohttpd
https://github.com/jonashaag/bjoern
Kilo Editor:https://github.com/antirez/kilo
ZeroMQ as C library for programming hispeed servers
ZeroMQ: https://zeromq.org/ and https://github.com/zeromq/libzmq
Programming servers in C with ZeroMQ becomes peace of cake:
https://rentry.co/DSRsecuritycourse-ZMQ
Picohttp - the fastest parser ever!
https://github.com/h2o/picohttpparser
twIP - an IP Stack in a Tweet - in 139 bytes of C!
twIP is a really, really tiny IP stack, written in 139 bytes of C code - small enough to fit in a Twitter message. Ok, so it is very far away from a real IP stack, but it can do the first task of an IP stack: respond to pings. The entire source code for version 1.1 can be found this tweet (139 characters long - version 1.0 in this tweet, 128 characters long).
https://dunkels.com/adam/twip.html
How complex is Assembler?
httpd in 100 LoC assembler: https://gist.github.com/DGivney/5917914
64 bit httpd in assembler: https://github.com/barrettotte/HTTP-ASM64/blob/master/server.asm
There is a shorter way: https://github.com/margaretbloom/nash-f :-)
General problem: Multithreading, Multicore and Synchronization
We're living in a new massive parallel core age. Go and Rust - by design are made for multicore. What problems do occurr?
How do we solve them? https://www.hillelwayne.com/post/learntla/
https://www.learntla.com/topics/optimization.html
The Binary Standard CDECL
CDECL: http://cdecl.org ; https://en.wikipedia.org/wiki/Calling_convention
Unix System V ABI: https://wiki.osdev.org/System_V_ABI#x86-64
(Un-)Marshalling: https://en.wikipedia.org/wiki/Marshalling_(computer_science)
https://bugaevc.github.io/asmwall/?cdecl
αcτµαlly pδrταblε εxεcµταblε: https://justine.lol/ape.html
C allows to generate automatic language bindings!
Example: https://www.gtk.org/docs/language-bindings/index
Complex in Python: https://docs.python.org/3/extending/extending.html
What Basic has to do with Assembler?
Basic almost is translatable 1:1 into Motorola 6502 Assembler. Same core ideas.
Learn old C64 programming! https://www.winz.run/c64/basic/index.html
The biggest money grave: Language bindings
https://ashvardanian.com/posts/porting-cpp-library-to-ten-languages/
https://www.google.com/search?q=c+c%2B%2B+binding+unmarshalling+-jaxb+-xml
Julia language to the rescue?
The "German Souvereign Tech fund" was founded as mainly "US independent" - that's why we called it 'souvereign' - organisation to sponsor software stacks of strategic importance or relevance.
See the unholy connection between http://iqt.org/portfolio and In-Q-Tel, an under cover CIA organization: https://en.wikipedia.org/wiki/In-Q-Tel
Cerebras, Julia Language, MemGraph, Databricks, Gitlab, Anaconda, Plotly, PubNub, MongoDB, TaxBit, VeraCode, Coudera, Cloudant, D-Wave, Palantir ... are all now CIA / NSA owned and thus backdoored!
Some years ago the US government allowed its employees (secret services included) to make upto $150,000 per year additional income from outside their official job. That has evolved into a total nighmare for the world. Insider informations from mass suveillance (see Edward Snowden and Julian Assange reports, XKeyscore) combined with full access to our computers and software?
US government is heavily financing almost the complete Open Source scene with their CIA guided military black budget of ~86 billion freshly printed dollars per year. (In fact they're printing 1 trillion dollars every 100 days!!!) May be the black budget is much higher now, but they're no longer publishing any informations about the volume for not giving their "enemies" insights into their "secret plans" taking over the world. Also see https://www.ned.org and reports / YouTube videos by Brian Berletic about this evil official US organisation, the propaganda arm of CIA.
The renewed US foreign surveillance act from 04/2024
https://www.whitehouse.gov/briefing-room/presidential-actions/2024/04/20/bill-signed-h-r-7888/
Schrems III EU court ruling to be expected soon
https://migosens.de/schlussantrag-zu-schrems-iii-liegt-vor-datenschutz-news-kw-17-2024/
The general problem of LLVM based languages
C++, Rust, Julia ... all are LLVM based. It has become a unmaintainable beast:
https://www.phoronix.com/news/LLVM-Record-Growth-2021
https://www.phoronix.com/news/Linux-Kernel-2021-Highlights
https://github.com/llvm/llvm-project/issues
The secure Eiffel programming language {P} C {P}
The "Hoare triple" {P} S {P}: https://en.wikipedia.org/wiki/Hoare_logic
{P} S {P} is called the "Hoare triple":
https://wwwmayr.in.tum.de/konferenzen/Jass08/courses/2/lang/paper_lang.pdf
https://www.eiffel.org/doc/eiffel/ET-_Design_by_Contract_%28tm%29%2C_Assertions_and_Exceptions
The Hoare Triple Theorem Prover
Your just invented algorithm you want to proof:
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
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/
The Hoare prover with Python/Z3: https://daltron.de/posts/hoare-prover/
https://github.com/gio54321/hoare-logic-prover/blob/master/examples/var_swap.lpp
What Z3 is capable to do:
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
https://ericpony.github.io/z3py-tutorial/fixpoint-examples.htm
Theory is from his 2011 paper: https://www.riec.tohoku.ac.jp/~unno/papers/pldi2011.pdf
More papers by Unno: https://www.riec.tohoku.ac.jp/~unno/
Captain Kirk solved this test: https://en.wikipedia.org/wiki/Kobayashi_Maru
Note: Without knowing Hoare Triple and Computer Science Notation no job in german security industry!
https://moves.rwth-aachen.de/wp-content/uploads/SS19/savos/exercises/ex-07.pdf
Learn Computer Science Metanotation!
Guy Steele: https://youtube.com/watch?v=7HKbjYqqPPQ
The most influencing two 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!!!
Are Unit Tests enough? What is Fuzzing doing? TLA+? Agda?
Unit Test only proof functionality of your implementation for a small set of parameters.
Fuzzing is randomly playing around with parameters and types, trying to detect "unsound" inputs. Problem here is, that the complete state space is not exhausively searched.
Example: int c := int a + int b; Here you only assume that the "+" implementation for 64 bit integers is correct.
With TLA+ proof system you can solve difficult (distributed, multitheaded) algorithms that might have timing (lock, deadlock) problems, like Paxos, Raft, ...: https://github.com/tlaplus/Examples TLA+ always permutates through the whole state space. So above example is far too much to be ever proven.
With mathematical proof systems like Agda (or Idris2) you only can mathematically proof that your algorithm is correct. It can proof with induction: n-> n+1. It only can proof single core / thread algorithms, does not solve possible timing problems that might occurr in multihreaded programs.
https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html
Agda uses dependent types that have solid mathematical foundation based on Peano and Zermelo-Fraenkel axioms.
Solvers like Z3, Picat or other SAT (SATisfiable) solvers are made to check constraints for given inputs: https://buttondown.email/hillelwayne/archive/picat-is-my-favorite-new-toolbox-language/ Picat is written in C and perfectly works together with other bash programs like awk, sed, tr, uniq, sort, bc, ...
Hackers are always watching out for holes in specs using undefined parameters, that might show up unpredicted functionalities that then can be exploited to insert own functionality.
How complex a compiler has to be? Fabrice Bellard's OTCC Compiler
http://bellard.org/otcc/
http://bellard.org/tcc/
https://github.com/c00kiemon5ter/ioccc-obfuscated-c-contest/blob/master/2001/bellard.hint
Looking into TCC code generation: https://briancallahan.net/blog/20220406.html
How fast a webserver can be?
Benchmarks:
5 million/sec: https://github.com/h2o/picohttpparser
1.2 million/sec: https://redbean.dev/
1 million/sec: https://github.com/jart/cosmopolitan/blob/master/examples/greenbean.c
Techempower benchmarks: https://www.techempower.com/benchmarks/
What languages do runtime range and bound checkings?
Rust?
Go?
Python?
FreePascal?
Dart?
Lisp?
Julia?
Smalltalk?
PHP?
JavaScript?
TypeScript?
C?
C++?
Eiffel?
D?
FFMpeg?
Gif Player?
Impact on energy consumption of programming languages
What impact on energy consumption have runtime range- and bounds checks?
Programming Languages transpiling to C as Intermediate Language
https://github.com/dbohdan/compilers-targeting-c
The Nim Programming language transpiles to C and JS!
German development by Andreas Rumpf: https://nim-lang.org/
Nim transpiles to JavaScript:
Lua / LuaJIT programming language
https://www.lua.org/
https://luajit.org by Michael Pall, Munich
https://luajit.org/dynasm.html
Lua for Android: https://github.com/damonkohler/sl4a
FreePascal / Lazarus the Borlard Delphi clone
Widely used in german Mittelstand:
Lazarus RAD IDE: https://www.lazarus-ide.org/
Modern OO Pacal language: https://www.freepascal.org/
FreePascal Benchmarks:
https://benchmarksgame-team.pages.debian.net/benchmarksgame/fastest/gcc-fpascal.html
FreePascal for Android: https://wiki.freepascal.org/Android
Professional Lazarus https://quartexdeveloper.com/
Handbook: https://www.blaisepascalmagazine.eu/en/product-category/books/
Classified as "safe language": https://readwrite.com/the-nsa-list-of-memory-safe-programming-languages-has-been-updated/
Webassembly as solution?
JSLinux - Linux Kernel running in your Browser
https://bellard.org/jslinux/vm.html?url=alpine-x86.cfg
You can follow this example on your own:
Webassembly on Servers (WASM)
https://medium.com/wasm/webassembly-on-the-server-side-c584f874b4a3
Compiling Go to Webassembly
https://github.com/nlepage/go-wasm-http-server
C to Webassembly with binaryen
https://github.com/WebAssembly/binaryen
Java to JS compiler by Google
https://github.com/google/j2cl/tree/master
https://www.wasm.builders/gunjan_0307/compiling-javascript-to-wasm-34lk
Compiling JS to Webassembly
https://www.wasm.builders/gunjan_0307/compiling-javascript-to-wasm-34lk
Awesome-Wasm-Langs
https://github.com/appcypher/awesome-wasm-langs
Have fun!
...
Up next lesson - https://rentry.co/DSRsecuritycoursepart0