Dennis Yurichev writes free books and notes on reverse engineering, assembly, and SAT/SMT solvers.
HN commenters recommend his SAT/SMT by Example as the best resource for the z3 solver, and link his mirror of Knuth's TeX errors paper.
Focusing on x86-64 (don't waste your time starting with the 32-bit variant when learning, let alone x87 FPU instructions, there's plenty of up-to-date materials for contemporary architectures nowadays):
- Chapter 10, Assembly Language (https://www3.nd.edu/~dthain/compilerbook/compilerbook.pdf#chapter.10) of http://compilerbook.org/
- intro_x86-64: Introduction to x86_64 assembly - https://gitlab.com/mcmfb/intro_x86-64
- Introduction to 64 Bit Assembly Language Programming for Linux and OS X
- Ray Seyfarth
- http://rayseyfarth.com/asm/
- Introduction to Computer Organization with x86-64 Assembly Language & GNU/Linux
- Robert G. Plantz
- http://bob.cs.sonoma.edu/IntroCompOrg-x64/book.html
- Modern X86 Assembly Language Programming
- 2018; Daniel Kusswurm
- Covers x86 64-bit, AVX, AVX2, and AVX-512
- https://github.com/Apress/modern-x86-assembly-language-programming-2e
- Understanding Assembly Language
- a.k.a. Reverse Engineering for Beginners; https://yurichev.com/blog/UAL/
- https://beginners.re/
- x86-64 Assembly Language Programming with Ubuntu
- Ed Jorgensen
- http://www.egr.unlv.edu/~ed/x86.html
- Assembly Programming and Computer Architecture for Software Engineers (APCASE)
- https://github.com/brianrhall/Assembly
- Videos: https://www.youtube.com/channel/UCr0svQEez3UQvlj6-5EYS6w
Or, if you prefer talks:
- Just enough Assembly for Compiler Explorer - Anders Schau Knatten
- NDC TechTown 2019
- https://www.youtube.com/watch?v=soeFwz0cOqU
- Modern…
A nice complement (and a generalization) of the MISRA C guidelines are the NASA/JPL C guidelines [1], which are also a very beautiful read. They can be succinctly summarized as ten simple rules [2] :
1. Avoid complex flow constructs, such as goto and recursion.
2. All loops must have fixed bounds. This prevents runaway code.
3. Avoid heap memory allocation.
4. Restrict functions to a single printed page.
5. Use a minimum of two runtime assertions per function.
6. Restrict the scope of data to the smallest possible.
7. Check the return value of all non-void functions, or cast to void to indicate the return value is useless.
8. Use the preprocessor sparingly.
9. Limit pointer use to a single dereference, and do not use function pointers.
10. Compile with all possible warnings active; all warnings should then be addressed before release of the software.
[1] https://yurichev.com/mirrors/C/JPL_Coding_Standard_C.pdf
[2] https://en.wikipedia.org/wiki/The_Power_of_10:_Rules_for_Developing_Safety-Critical_Code
Starting back around 2009, I started marking bug fixes in git with the first line containing "Bug fix---description". For example (from my gopher server [1]):
a12c3fd Bug fix---sample forgot POST method.
0b1bce2 Bug fix---grab guid when only given numeric uid.
31408da Bug tracking---crash because filename is nil?
d993265 Bug fix---Clean the display text to prevent broken index files.
47e98e8 Bug fix---line comments were broken in .port70 files.
I do the same at work. I got the idea from Donald Knuth, who wrote a paper about classifying each error in TeX [2]. I didn't go as far as he did, but I still have his list handy:
* Algorithm
* Blunder
* Cleanup
* Data
* Efficiency
* Forgotten
* Generalization
* Interaction
* Language
* Mismatch
* Portability
* Quality
* Robustness
* Surprise
* Typo
[1] https://github.com/spc476/port70
[2] "The Errors of TeX" <https://yurichev.com/mirrors/knuth1989.pdf>
These are other good resources:
- rise4fun https://rise4fun.com/z3/tutorialcontent/guide
- https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- Programming Z3 -https://theory.stanford.edu/~nikolaj/programmingz3.html
- Nikolaj Bjorner's tutorial https://youtu.be/nGwyNmsxX6I
- Hakank's examples http://www.hakank.org/z3/
- Yurichev's book "SMT by Example" https://yurichev.com/writings/SAT_SMT_by_example.pdf
- http://hackage.haskell.org/package/sbv
- https://www.youtube.com/watch?v=ruNFcH-KibY Tikhon Jelvis - Analyzing Programs with Z3
- https://www.youtube.com/watch?v=rvPWDgJc0O4&ab_channel=ACMSIGPLAN - Nadia Polykarpova on Z3
- SAT SMT school https://sat-smt.in/
- Emina Torlak's course https://courses.cs.washington.edu/courses/cse507/19au/calendar.html
- Lindsey Kuper - SMT Solving and Solver-Aided Systems http://composition.al/CSE290Q-2019-09/
- http://www.sc-square.org/CSA/school/lectures.html
The problem with Ada, was the price of the compilers, and that the few UNIX vendors that bothered with Ada, like Sun, it was an additional license on top of the already expensive SunOS/Solaris Developer SDK.
Thus the push for C and C++, alongside security certifications, where those languages feel like using Ada with a C like syntax.
https://www.perforce.com/blog/kw/NASA-rules-for-developing-safety-critical-code
https://yurichev.com/mirrors/C/JPL_Coding_Standard_C.pdf
https://misra.org.uk/
Nowadays we live in a world where developers refuse to pay for their tools like other professionals, but hey, Rust is free beer, not like the several millions per seat licenses used by Ada vendors, of whom there are still 7 vendors in business.
This paper is a case study of program evolution. The author kept track of all changes made to TEX during a period of ten years, including the changes made when the original program was first debugged in 1978. The log book of these errors, numbering more than 850 items, appears as an appendix to this paper. The errors have been classified into fifteen categories for purposes of analysis.
I came to the conclusion that the designer of a new system must not only be the implementor and the first large-scale user; the designer should also write the first user manual. - Donald Knuth, 'The Errors of TeX' (1989) https://yurichev.com/mirrors/knuth1989.pdf (4.8MB)
... via https://github.com/globalcitizen/taoup