ver 0.1: 2017-08-16
ver 0.1.1: 2017-08-17
Pentesting is a search algo for vulns. The goal is falsifying the proposition that the target fulfills its security specs (which might not be provided by the client and needs to be generated by the pentester from docs and convos). Not coincidentally, this is the same technique for generating proofs in automated theorem proving. Searching for contradictions is a common approach to proving theorems. This is essentially pentesting the theorems.
There are various strategies1 with which you choose the next tactic. One example of a tactic is induction. One strategem2 is to backtrack – start from the target statement and work backwards. Its reverse is forward propogation – start from the known statements and derive more statements, with some other strategem to inform what tactics to apply to get new statements. See below for more on tactics. Generally, if there is a Formal Methods concept, it can be applied to pentesting.
When I start a pentest, I just look around, looking at whatever catches my eye, searching for hints of good and bad. At the same time I look for goodness, and get a grip on how the target behaves, what it’s supposed to do, and whether it really is doing that. I try to exercise all the functionality. I call this the spray-and-pray strategy. This part is entirely intuitive and I’m not going to attempt here to connect it to anything I have seen in Formal Methods.
After the regular walk-through and spray-and-pray, I list out all the security specs and a percentage on how confident I am in them. (I never write 100%. If I write 99% it means I’m not coming back to it.) These are not formal specs, but the more I can formalize them, the more logic holes I can catch. Then I use both the meet-in-the-middle and conflict-driven strategems to develop attacks or assert safety (within assumptions). See below for more on strategems.
Now if everything checks out with the first spec, I go back and make it more detailed. I think about all the classes of attacks to inform your spec. When I read over the spec, if I don’t find any holes, then I go do research, read vuln articles for inspiration, or take a nap. I might just find a hole in my spec. Also, I have found that keeping work and play separate doesn’t work that well. Some times I dream of personal things, some times I dream of vulns for work. No matter what, when I get up, I have to write those down.
One of my favorite practical strategems, inspired by the cryptanalysis technique of the same name, and reinforced by an offhand comment by Leino3, is meet-in-the-middle. You alternate forward propagation and backtracking. This can reduce the complexity of the algorithm a ton, depending on where you meet in the middle, and the size of the search space. I intend to write another post on a math puzzle where I detail how I used this approach.
Another strategem is Conflict-Driven Clause Learning (CDCL)4 which I am not deeply familiar with in Formal Methods, but has inspired my pentesting methods. While CDCL has a technical definition, the key point in practice is to use conflicts to prune your searches. Argue with yourself, have a little blue team in your mind and a red team. One tries to argue that there is no vuln, the other that there is. Take turns poking holes in each side’s argument, i.e. search for statements that refute the other’s claim, then this will lead to more statements. Now poke holes in these new statements from the other side’s perspective.
TODO
There has been research into how to make proof searches more human-like5. Perhaps the methods of pentesters can be fruitful in developing these methods.
Thanks to person A’s comments and suggestions, this article flows much better and is better organized.
The technical term is “heuristics”. I prefer “strategy” in this article, and “strategems” for strategic concepts that inform your strategy. ↩
A concept that informs the construction of a strategy. The strategy ultimately tells you what tactic to choose in any given situation. ↩
a person who works on Dafny ↩
https://profs.scienze.univr.it/~bonacina/papers/AFM2017cdr.pdf ↩
TODO ↩