HACKE-RC

PML4

pwndbg> p/x (*PML4).entries
$5 = {{
    value = 0x100001007
  }, {
    value = 0x0
  } <repeats 255 times>, {
    value = 0x100002007
  }, {

HACKE-RC

Satisfiability Modulo Theories (SMT) solvers are one of the most interesting topics to learn about in Computer Science. When you first discover them, they feel surprising and magical. You might already have heard of or seen someone use a SMT solver like Z3 for solving CTF challenges or Program Analysis and by the end of this video, you'll have a good grasp of all the required knowledge to get started and use Z3.

I will not use any complicated mathematics to explain these solvers and will deal with only required theory and examples.

SAT Solvers

SMT solvers leverage the powers of another type of solvers called Boolean Satisfiability Problem solvers. As the name suggests, they have something to do with Boolean variables.

These solvers basically take a Boolean expressions and output whether there are possible values for the Boolean variables which result in the expression being true (or satisfiable). When there are no such variables SAT solver outputs unsatisifable.

If the expression is satisfiable t

HACKE-RC

from z3 import *

square = Int("square")
circle = Int("circle")
triangle = Int("triangle")

solver = Solver()
solver.add(square * square + circle == 16)
solver.add(triangle * triangle * triangle == 27)
solver.add(triangle * square == 6)

HACKE-RC

Common calling conventions

• cdecl
• fastcall
• stdcall

CDECL calling convention.

cdecl stands for "C declaration", it is used by most c compiler in the x86 architecture.

Arguments passing in cdecl calling convention

HACKE-RC

#inlclude <windows.h>
#include <stdio.h>
// function to set a environment variable globally by editing the registry keys.
NTSTATUS SetEnvironmentVariableR(LPCSTR lpName, LPCSTR lpValue){
    HKEY hKey; // this will hold the handle to the registry key.
    
    // We are going to open the registry key for HKEY_CURRENT_USER\Environment.
    RegCreateKey(HKEY_CURRENT_USER, "Environment", &hKey);
    
    // Error check.

HACKE-RC

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace CLRHello1
{
	class Program
	{

HACKE-RC

import winim/clr

# buffer contains the dll
var buf: array[3584, byte] = [
    byte 0x4D, 0x5A, 0x90, 0x00, 0x03, 0x00, 0x00, 0x00, 0x04, 0x00, 0x00, 0x00,
    0xFF, 0xFF, 0x00, 0x00, 0xB8, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
    0x40, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
    0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
    0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
    0x80, 0x00, 0x00, 0x00, 0x0E, 0x1F, 0xBA, 0x0E, 0x00, 0xB4, 0x09, 0xCD,

HACKE-RC

struct _KTHREAD {
  struct _DISPATCHER_HEADER Header;
  void *SListFaultAddress;
  unsigned int QuantumTarget;
  void *InitialStack;
  void *StackLimit;
  void *StackBase;
  unsigned int ThreadLock;
  unsigned int CycleTime;
  unsigned long CurrentRunTime;

HACKE-RC

struct _ETHREAD {
  struct _KTHREAD Tcb;
  union _LARGE_INTEGER CreateTime;
  union _LARGE_INTEGER ExitTime;
  struct _LIST_ENTRY KeyedWaitChain;
  void *ChargeOnlySession;
  struct _LIST_ENTRY PostBlockList;
  void *ForwardLinkShadow;
  void *StartAddress;
  struct _TERMINATION_PORT *TerminationPort;

HACKE-RC

struct _TEB {
  struct _NT_TIB NtTib;
  void *EnvironmentPointer;
  struct _CLIENT_ID ClientId;
  void *ActiveRpcHandle;
  void *ThreadLocalStoragePointer;
  struct _PEB *ProcessEnvironmentBlock;
  unsigned long LastErrorValue;
  unsigned long CountOfOwnedCriticalSections;
  void *CsrClientThread;