integeruser · July 6, 2019 16:15 · Jun 28, 2017
diff --git a/flags.py b/flags.py
@@ -0,0 +1,37 @@
+#!/usr/bin/env python2
+# -*- coding: utf-8 -*-
+#
+# Retrieve back names of header file constants
+#
+# $ ./flags.py PROT 5
+# PROT_EXEC           0x4
+# PROT_NONE           0x0
+# PROT_READ           0x1
+# PROT_WRITE          0x2
+# 5 or 0x5 is PROT_READ|PROT_EXEC
+
+import argparse
+
+import pwnlib
+import z3
+
+parser = argparse.ArgumentParser()
+parser.add_argument('type', choices=['AF', 'MAP', 'PROT', 'MSG', 'O', 'PR', 'PTRACE', 'SIG', 'SIGEV', 'SOCK', 'SYS'])
+parser.add_argument('value', type=int)
+parser.add_argument('--os', default='linux')
+parser.add_argument('--arch', default='amd64')
+args = parser.parse_args()
+
+with pwnlib.context.context.local(os=args.os, arch=args.arch):
+    consts = [getattr(pwnlib.constants, item) for item in dir(pwnlib.constants) if item.startswith(args.type + '_')]
+    for const in sorted(consts, key=int):
+        print '%-20s%s' % (const, hex(int(const)))
+
+z3vars = [z3.Bool(str(const)) for const in consts]
+
+solver = z3.Solver()
+solver.add(args.value == z3.Sum([z3var * int(const) for z3var, const in zip(z3vars, consts)]))
+
+if solver.check() == z3.sat:
+    model = solver.model()
+    print '%d or %s is %s' % (args.value, hex(args.value), '|'.join(str(z3var) for z3var in model if model[z3var]))