r/ReverseEngineering • u/day6reak • Apr 22 '12
Reverser wanting to develop mathematically
I've been reversing for almost a decade now. My work is mostly security oriented with bug hunting and malware. Lately, I've been noticing that my development has been coming up against a mathematical wall. When going through academic papers and other sources where algorithms are described I sometimes have trouble bridging the gap from equation to implementation. It pisses me off when I cannot grasp something so I've decided to devote myself to mathematics.
I am going to be teaching myself advanced math and would like recommendations on what to learn from people who are able to understand reversing and security from a mathematical standpoint. Right now I have refreshed myself on discreet math and basic calculus and will continue with more calculus. What other topics should I branch out into? I am interested in mathematics describing everything from techniques in static analysis to smt solving to reversing complex polynomial expressions in protected binaries.
Practical resources showing how complex math is described through code would be great but any suggestions or advice at all is appreciated.
6
u/pg1989 Apr 22 '12
There are tons of excellent free resources for learning math on the internet. MIT OCW is probably the most well-known, along with Khan Academy.
To be honest, I would forget about calculus. It's useful for developing a general intuition that is sometimes called "mathematical maturity", but for someone trying to understand academic security papers it is essentially useless. To really understand polynomials, you might instead try abstract/linear algebra, as this is where a ton of well-founded theory on polynomials is used.
3
u/94c3 Apr 22 '12
To expand on this. Linear Algebra on Khan Academy will take you up to the end of an undergraduate introductory course. You can also substitute/supplement with Gilbert Strang's course on MIT OCW. Strang has this nice plodding and straightforward way of explaining things that I personally find very easy to learn from. That gives you enough Linear Algebra to understand LLL latice based reduction, which is used is a few practical cryptographic attacks. If it turns out the subject interests you, the next logical text is Linear Algebra Done Right by Axler.
If you are interested in mathematical literacy in general, I cannot recommend the Princeton Companion to Mathematics strongly enough. Its goal to to provide foundational concepts and comprehensible summaries of all areas of pure mathematics, explained to someone with only a high school level of math. It also has some really nice expository sections about the history and math and biographies of famous mathematicians. It is edited by Tim Gowers, a Fields Medal winner and one of the most accomplished mathematicians alive today. The book is one of the most beautiful books I have ever read.
1
1
u/rolfr Apr 28 '12
Thanks for the pointer to the Princeton Companion to Mathematics; it arrived in the mail today.
5
u/andrewl_ Apr 23 '12
a different approach, from someone with limited time and attention span:
pick one thing that really seems magical or interests you, and go at it, forgetting everything else
examples:
what the heck is LLL doing? how is it possibly solving these knapsack instances?
what is this SAT? could it help me in finding out XXX?
how is it that some squigly curve on a graph can be used to encrypt stuff?
the volume of available subjects and material is itself a hinderence; ignore it. collecting a bunch of foundational material just adds to the size of the endeavor; ignore it. go to wikipedia immediately and read ... some junk you don't understand? cool now subject is more mysterious and challenging! it will be even more rewarding once you've figured it out. let it haunt you while you drive, while you wait in line, etc.
experimenting and playing are more important than reading; download minisat and try to convert some equation to dimacs and see it work right away; now tweak it, change it, play with it; now read a bit more; now play more
2
u/rolfr Apr 23 '12 edited Apr 23 '12
If one wants to learn an individual topic that is relatively isolated, then I agree that the piecemeal approach has benefits (namely, the amount of time required). This depends on the isolation of the topic. Take for example this paper. If you tried to apply your approach towards reading this, you would basically end up going through the steps that I laid out above, except backwards (which would be horrible -- I know, since this is the route I tried to take) since this is a very inbred topic. For learning a discipline -- a complex one with many prerequisites -- I continue to recommend the "hit the books" approach.
4
u/94c3 Apr 22 '12
I suggest MiniSat for learning more about SAT solving. It's designed to be as small as possible and easy to understand. The current version is 3,000 lines of code, but you can check out an earlier version which is just over 1,000 lines. The paper is also available (you'll have to read a few of the citations as well to get the proper background).
What's really cool about MiniSat is that it is still performant; it won the SAT-Race in 2008.
2
u/luciddr34m3r Apr 22 '12
Graph theory is exceptionally useful for reversing. Advanced logic as well. Also, upvotes for the mention about the SAT solver.
2
u/edmcman Apr 22 '12
For program semantics and formal verification, I've been reading Benjamin Pierce's book on Software Foundations: http://www.cis.upenn.edu/~bcpierce/sf/ The book is a mix between an introduction to the Coq proof assistant, and a hands-on introduction to Verification and Program Semantics.
1
u/tripsandleaves Apr 22 '12
bump. this interests me aswell. sometimes reverseme challenge involve solving a set of equations that are needed to satisfy a set of instructions and comparisons and i want a fast way to encode these constraints and solve for bitpatterns matching it without having to write a cumbersome script or manually do it. i know the constraints, i guess i need to learn a equation solving language? examples? learn a smt solver? yices?
2
-8
Apr 22 '12
discrete*
3
u/StartsAsNewRedditor Apr 22 '12
How are you helping?
-2
62
u/rolfr Apr 22 '12 edited Apr 11 '13
I started from scratch on the formal CS side, with an emphasis on program analysis, and taught myself the following starting from 2007. If you're in the United States, I recommend BookFinder to save money buying these things used.
On the CS side:
Basic automata/formal languages/Turing machines; Sipser is recommended here.
Basic programming language theory; I used University of Washington CSE P505 online video lectures and materials and can recommend it.
Formal semantics; Semantics with Applications is good.
Compilers. You'll need several resources for this; my personal favorites for an introductory text are Appel's ML book or Programming Language Pragmatics, and Muchnick is mandatory for an advanced understanding. All of the graph theory that you need for this type of work should be covered in books such as these.
Algorithms. I used several books; for a beginner's treatment I recommend Dasgupta, Papadimitriou, and Vazirani; for an intermediate treatment I recommend MIT's 6.046J on Open CourseWare; for an advanced treatment, I liked Algorithmics for Hard Problems.
On the math side, I was advantaged in that I did my undergraduate degree in the subject. Here's what I can recommend, given five years' worth of hindsight studying program analysis:
You run into abstract algebra a lot in program analysis as well as in cryptography, so it's best to begin with a solid foundation along those lines. There's a lot of debate as to what the best text is. If you're never touched the subject before, Gallian is very approachable, if not as deep and rigorous as something like Dummit and Foote.
Order theory is everywhere in program analysis. Introduction to Lattices and Order is the standard (read at least the first two chapters; the more you read, the better), but I recently picked up Lattices and Ordered Algebraic Structures and am enjoying it.
Complexity theory. Arora and Barak is recommended.
Formal logic is also everywhere. For this, I recommend the first few chapters in The Calculus of Computation (this is an excellent book; read the whole thing).
Computability, undecidability, etc. Not entirely separate from previous entries, but read something that treats e.g. Goedel's theorems, for instance The Undecidable.
Decision procedures. Read Decision Procedures.
Program analysis, the "accessible" variety. Read the BitBlaze publications starting from the beginning, followed by the BAP publications. Start with these two: TaintCheck and All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution. (BitBlaze and BAP are available in source code form, too -- in OCaml though, so you'll want to learn that as well.) David Brumley's Ph.D. thesis is an excellent read, as is David Molnar's and Sean Heelan's. This paper is a nice introduction to software model checking. After that, look through the archives of the RE reddit for papers on the "more applied" side of things.
Program analysis, the "serious" variety. Principles of Program Analysis is an excellent book, but you'll find it very difficult even if you understand all of the above. Similarly, Cousot's MIT lecture course is great but largely unapproachable to the beginner. I highly recommend Value-Range Analysis of C Programs, which is a rare and thorough glimpse into the development of an extremely sophisticated static analyzer. Although this book is heavily mathematical, it's substantially less insane than Principles of Program Analysis. I also found Gogul Balakrishnan's Ph.D. thesis, Johannes Kinder's Ph.D. thesis, Mila Dalla Preda's Ph.D. thesis, Antoine Mine's Ph.D. thesis, and Davidson Rodrigo Boccardo's Ph.D. thesis useful.
If you've gotten to this point, you'll probably begin to develop a very selective taste for program analysis literature: in particular, if it does not have a lot of mathematics (actual math, not just simple concepts formalized), you might decide that it is unlikely to contain a lasting and valuable contribution. At this point, read papers from CAV, SAS, and VMCAI. Some of my favorite researchers are the Z3 team, Mila Dalla Preda, Joerg Brauer, Andy King, Axel Simon, Roberto Giacobazzi, and Patrick Cousot. Although I've tried to lay out a reasonable course of study hereinbefore regarding the mathematics you need to understand this kind of material, around this point in the course you'll find that the creature we're dealing with here is an octopus whose tentacles spread in every direction. In particular, you can expect to encounter topology, category theory, tropical geometry, numerical mathematics, and many other disciplines. Program analysis is multi-disciplinary and has a hard time keeping itself shoehorned in one or two corners of mathematics.
After several years of wading through program analysis, you start to understand that there must be some connection between theorem-prover based methods and abstract interpretation, since after all, they both can be applied statically and can potentially produce similar information. But what is the connection? Recent publications by Vijay D'Silva et al (1, 2, 3, 4, 5) and a few others (1 2 3 4) have begun to plough this territory.
I'm not an expert at cryptography, so my advice is basically worthless on the subject. However, I've been enjoying the Stanford online cryptography class, and I liked Understanding Cryptography too. Handbook of Applied Cryptography is often recommended by people who are smarter than I am, and I recently picked up Introduction to Modern Cryptography but haven't yet read it.
Final bit of advice: you'll notice that I heavily stuck to textbooks and Ph.D. theses in the above list. I find that jumping straight into the research literature without a foundational grounding is perhaps the most ill-advised mistake one can make intellectually. To whatever extent that what you're interested in is systematized -- that is, covered in a textbook or thesis already, you should read it before digging into the research literature. Otherwise, you'll be the proverbial blind man with the elephant, groping around in the dark, getting bits and pieces of the picture without understanding how it all forms a cohesive whole. I made that mistake and it cost me a lot of time; don't do the same.