Jay Kruer - Vita


  • Amal Ahmed, Northeastern University, Boston, MA: amal@ccs.neu.edu
  • Cody Roux, Draper Laboratory, Boston, MA: croux@draper.com
  • Education

    Bachelor of Arts (BA) in Mathematics and Computer Science
    Reed College, Portland, Oregon
    8/2016 -


    Black Hat USA Student Scholarship
    Black Hat USA, Las Vegas, NV
    Summer 2017

    Academic Commendation
    Reed College, Portland, OR


    Visiting Scholar

    Programming Research Laboratory at Northeastern University, Boston, MA
    1/2019 -
    Advisor: Amal Ahmed
  • I am spending the spring of 2019 at Northeastern mechanizing in Coq the metatheory of Oxide, a language modeling Rust.
  • Code
  • Proof of type-safety for STLC with bools using a well-scoped de Bruijn representation.
  • Talks
  • Operational Semantics for Multi-language Programs (2/2019)
  • Intern

    The Charles Stark Draper Laboratory, Cambridge, MA
    6/2018 - 8/2018
    Supervisor: Cody Roux
  • Implemented and verified string sanitization routines written in C and WhyML using Frama-C and Why3 and Coq
  • Developed an automated build instrumentation system to test the static analysis capabilities of mainstream C compilers
  • Developed an automated testing system that generates a report based on the result of running exploit payloads against vulnerable binaries with various runtime mitigations applied
  • Generated a collection of vulnerable C programs and exploit payloads to test the systems mentioned above across an array of vulnerability scenarios and exploitation techniques
  • Teaching Assistant

    CSCI 221: CS Fundamentals II
    My blurb: An introduction to higher-level reasoning about programming through digital logic, assembly programming, functional programming in Standard ML, and concurrent programming in Go.
    Reed College, Portland, Oregon
    Instructors: Eitan Frachtenberg, Kelly Shaw
    8/2017 - 12/2017

    Teaching Assistant

    CSCI 121: CS Fundamentals I
    My blurb: An introduction to programming and computer science principles through Python.
    Reed College, Portland, Oregon
    Instructors: Jim Fix, Adam Groce
    8/2017 - 12/2017


    Computer User Services
    Reed College, Portland, Oregon
    Supervisor: Taylor Smith
    10/2016 - 5/2017


  • Type theory
  • Basic category theory
  • Pure mathematics: analysis (elementary/non-measure theoretic); discrete mathematics (combinatorics, discrete probability, and elementary number theory); linear algebra; abstract algebra; vector calculus and analysis
  • Automated theorem provers: Frama-C and Why3
  • Coq
  • Standard ML
  • OCaml
  • Python
  • C
  • Rust
  • Go
  • x86* assembly
  • Reverse engineering
  • Git
  • LaTeX
  • Mandarin Chinese: advanced literary proficiency, roughly HSK 6+
  • Classical Chinese: working proficiency
  • Conferences attended

    DEF CON (security conference)
    Las Vegas, NV

    Black Hat USA (security conference)
    Las Vegas, NV

    DerbyCon (security conference)
    Louisville, KY