Skip to content

Instantly share code, notes, and snippets.

View dvtate's full-sized avatar
🐧
chilling

Dustin Van Tate Testa dvtate

🐧
chilling
161 followers · 107 following
View GitHub Profile
@tothi
tothi / ms-msdt.MD
Last active September 29, 2024 08:10
The MS-MSDT 0-day Office RCE Proof-of-Concept Payload Building Process

MS-MSDT 0-day Office RCE

MS Office docx files may contain external OLE Object references as HTML files. There is an HTML sceme "ms-msdt:" which invokes the msdt diagnostic tool, what is capable of executing arbitrary code (specified in parameters).

The result is a terrifying attack vector for getting RCE through opening malicious docx files (without using macros).

Here are the steps to build a Proof-of-Concept docx:

  1. Open Word (used up-to-date 2019 Pro, 16.0.10386.20017), create a dummy document, insert an (OLE) object (as a Bitmap Image), save it in docx.
@SegHaxx
SegHaxx / pcbooter.s
Created November 30, 2021 22:03
PC bootsector string spewer in NASM
; vi:ft=nasm
cpu 8086
org 0x0
jmp start
rulz db 'seg rulz ok ',0
start: cli ; disable interrupts because lolbugs
mov ax,0x7c0 ; BIOS loads code at 0000:7C00
@TheTimgor
TheTimgor / rotate.py
Created March 5, 2021 07:51
def fast_rot(width, height, raster):
for j in range(0, width):
for k in range(0, height):
to = width * height - (height * j + k + 1)
i = (width - j - 1) + width * k
if i != to:
while i > to:
i = width * (height - (i % height) - 1) + ((i - (i % height)) / height)
buffer = raster[int(i)]
raster[int(i)] = raster[int(to)]
@mstewartgallus
mstewartgallus / nonsense.v
Created February 20, 2021 19:51
(* mostly cribbing from https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html and nlab *)
(*
A topos has has finite limits, is cartesian closed, and has a subobject classifier. I guess ? *)
(* FIXME cleanup notation levels *)
Inductive object : Set :=
| terminal
| tuple (_ : object) (_: object)
| fn (_ : object) (_: object)
@mstewartgallus
mstewartgallus / somethinglikebidi.v
Last active February 8, 2021 01:19
I was trying to understand bidirectional typechecking so I tried a similar approach in Coq of specifying inference rules and wellformed rules separately. No idea if this works as a type system but it seems to handle non-strictly positive recursion much better.
Section s1.
Variable v : Set.
Inductive term : Set :=
| var : v -> term -> term
| typ : term
| set : term
| app : term -> term -> term
| all_ : term -> (v -> term) -> term
| lam_ : term -> (v -> term) -> term
@mstewartgallus
mstewartgallus / executionplan.v
Last active January 24, 2021 05:53
Inductive expr : Set :=
| lit : nat -> expr
| add : expr -> expr -> expr.
(* Define the type of big step semantics *)
Inductive big : expr -> nat -> Prop :=
| big_lit : forall x, big (lit x) x
| big_add : forall x y a b, big x a -> big y b -> big (add x y) (a + b).
(* A step maps a state to a state *)
@mstewartgallus
mstewartgallus / hoas.makam
Created January 24, 2021 04:01
The hoas support is kind of neat but idk.
%open syntax.
%extend kz.
obj : type.
terminal : obj.
fn : obj -> obj -> obj.
tuple : obj -> obj -> obj.
typ : type.
@mstewartgallus
mstewartgallus / kappa.makam
Last active January 23, 2021 02:19
Tried out makam (lambda Prolog dialect) http://astampoulis.github.io/makam/ . Remarkable velocity although poor tooling.
%open syntax.
expr : type.
id : expr.
compose : expr -> expr -> expr.
bang : expr.
v : (_ : string) -> expr.
@mstewartgallus
mstewartgallus / sequents.pro
Last active July 28, 2022 05:16
Sequent Calculus style stuff with Prolog. I could probably handle variables better in the future and also improve the DSL a bit. Different search strategies would probably be necessary in a full thing.
:- use_module(library(clpfd)).
:- use_module(library(dcg/basics)).
:- op(1150, xfy, user:(———————————————————————————————————)).
:- op(980, xfy, user:(~~>)).
:- op(980, xfy, user:(~>)).
:- op(980, xfy, user:(*~>)).
:- op(950, xfx, user:(⊨)).
@mstewartgallus
mstewartgallus / kappacesk.hs
Last active January 15, 2021 22:45
Latest Cesk kappa calculus interpreter
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeFamilies #-}