Reversing the Petya ransomware with constraint solvers
0xec.blogspot.com
0xec.blogspot.com
In 1991, my company was sandboxing commercial software. This was for try-before-you-buy. Except, instead of recompiling a crippled version, we would take a retail SKU, encipher the executables and then deliver with a device driver: a VxD. The VxD would hook the low level Int13 IO calls to pass all disk IO through a write-through cache. The installed app could read from anywhere on the disk. But, all attempts to write would copy the changed sectors to the cache. This would allow a perfect uninstall; simply remove the cache and the disk reverts back to its preinstalled state. This was because most software, back in 1991, assumed that you'd never want to uninstall. So, it would scatter its junk all over the place.
Now imagine if the VxD was part of the OS. Any downloaded exe could access the HD, but all writes would write-through to a separate cache. That was 25 years ago. This is a roundabout way of asking: how feasible is sandboxing to avoid malware?
The trouble with root access is that there's always a way for active malice to get in. For instance, our approach is trivially vulnerable to loading a kernel module. It's possible that something like user namespaces would solve that today.
This call does not change the current working directory, so that after the call '.' can be outside the tree rooted at '/'. In particular, the superuser can escape from a "chroot jail" by doing:
mkdir foo; chroot foo; cd ..
However, there are some kernel patches floating around that disable double-chroot, so just as such an attack would be easy, blocking that specific attack would be easy too. My point was that there are lots of things that root can do, and blocking them all is difficult; in general root is trusted to load drivers, which means it can bypass any driver that confines it. There's no direct equivalent of chroot on 16-bit DOS/Windows, but you could almost certainly bypass OP's filtering scheme by loading your own VxD that fought with theirs.
chdir("/"); /* go to / of "chroot jail" */
mkdir("foo", ...); /* create directory in jail */
chroot("foo"); /* change / to foo */
/* fail to chdir("foo"); */
chdir(".."); /* instead go up parent (there is nothing preventing you since you are no longer in the "chroot jail" since the jail is now foo and you never entered it) */
chdir("..");
/* ... */
chdir(".."); /* . is now the real root */
chroot("."); /* change / to the real root */
Note that this includes Linux itself with CLONE_NEWNS + pivot_root (which is what Docker does).
Parent's attack requires the attacker to have root inside the chroot. It's a "double-chroot" attack: you call chroot a second time as root, so a new directory starts getting remapped. Then the old one no longer does, and you can "cd .." out of it and eventually "chroot ." when you get to the top. The only mitigation is not to give an attacker root inside a chroot.
Your attack does not require the attacker to have root. Instead, the process who was setting up the chroot (which does have root) forgets to cd into the chroot, and leaves the working directory outside it. The attacker cannot chroot again, but they can continue to cd anywhere on your filesystem.
It does exactly what you want, although it was created for different use cases (Live CDs, layered images as used by Docker, etc.):
https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux....
Means you assert a result on a variable at the end, specify which variables and states will affect the wanted result, and the framework and solver will efficiently backtrack all the possible solutions of input variables to come up to your desired endstate, by filtering out impossible paths and values. Like in a game.
Z3 is very popular, because you can write your problem in python. Ages ago lisp was very popular, and some of the very first lisp programs from the 60ies were such solvers (general planner) leading to AI. And recently with the implementation of efficient simple open-source SMT solvers (minisat, ...) implemented within gcc or llvm you can now even use normal C programs and backtrack results, optimize and check types, do bounds checking, generate tests from bugs and so on. This is not comparable to simple fuzzing or brute-forcing, it knows the program flow, and works the flow backwards.
If any algorithm can be weakened by such 'problem solvers', it wouldn't be considered strong? For instance, can SHA256 be reversed (i.e. collision found) faster with such a solver? I guess not..
I realize that with crypto, solvers can optimize the flow of the algorithm, make it more efficient and omit repeating some code parts, but a good bruteforcer written in assembly can be as optimized..?
In general most crypto can't be broken by solvers. The solvers might be faster than brute force, but still take exponential amounts of time to solve it. However if the crypto was designed badly, there can be weaknesses in it that the solvers can find and exploit.
It's basically like those logic puzzles that are sometimes asked to kids. I don't have a specific example handy, but they go like "Fred won't sit next to Bill. Bill wants to sit next to Mary. Mary wants to sit in the same table as Ned..." And then they ask you to find a seating arrangement that satisfies all these constraints.
You can try every possibility, and there are exponentially many as you add more people. But if you are clever, you can realize certain constraints rule out large portions of the search space. Like you know the answer must have Mary in the same table as Ned, so you don't even try any possibilities where that's not true. There are many other clever tricks SAT solvers use to shrink the search space.
[1]: https://gist.githubusercontent.com/extremecoders-re/499d4617...
Not the most useful encryption method though.
> Brute force search should not be confused with backtracking, where large sets of solutions can be discarded without being explicitly enumerated *
> solver will efficiently backtrack all the possible solutions of input variables to come up to your desired endstate, by filtering out impossible paths and values
That seems to be a contradiction, because Back-Tracking uses Brute-Force. The efficiency comes from heuristics that can fail, which is kind of important to note. SAT problems are in principle np-complete with all the uncertainty that implies.
Any links to examples of the above?
klee: https://klee.github.io/tutorials/ pretty hard to install
coq: https://coq.inria.fr/a-short-introduction-to-coq the real beast out there. easy to install. but hardly usable for normal hackers, because of their mathematical notation. but it's using plain c, and you can verify c with various solvers.
z3: http://rise4fun.com/z3/tutorial the most popular, but only python or SMT-LIB 2.0 (lisp).
for crypto https://srlabs.de/minisat-intro/ has some explanation how to break weak ciphers or hashes, knowing the weakness beforehand. but the various hackers posting on their blogs usually have better practical explanations.
:)
The author made it look so easy to reverse this. Kudos, and thanks for the community service.
fwiw I've been using various flavors of linux for years(CentOS/Arch/FreeBSD lately) for everything but a single dev laptop I keep Windows for testing/native apps.
My comment wasn't meant to be advocating Windows, let alone XP, I just thought it was funny.
As they say, Don't' roll your own crypto.
I have a feeling the malware author, working in 16-bit realmode, forgot that ints are usually 16 bits wide in that environment. A "typedef unsigned int uint32_t" behaves as expected in the usual 32/64-bit environment, but not in 16-bit. It's unlikely the author invented the 16-bit Salsa20 variant, but rather copied existing code and just compiled it wrongly.
I wonder what happens with FAT32, or does it just do a stupidly simple "encrypt the first n sectors of the disk"?