Lobster Roll

This paper summarizes my experience in implementing a compiler for a functional language. The language is ML1 [Milner 84] and the compiler was first implemented in 1980 as a personal project when I was a postgraduate student at the University of Edinburgh2. In this paper, “the” ML compiler refers...

From the abstract: > This thesis presents a type system combining ML-style parametric polymorphism and subtyping, with type inference, principal types, and decidable type subsumption. Type inference is based on biunification, an analogue of unification that works with subtyping constraints. Ba...

An interesting paper that surveys symbolic execution techniques, but there are [an accompanying set of slides](https://github.com/ercoppa/symbolic-execution-tutorial/blob/master/symbolic-execution.pdf) as well now that may be interesting as well for a re-submission. The article talks about what ...

From the abstract: > Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility and code reuse ...

If you missed it, [FireEye suffered a breach and as a result certain threat actors gained access to their red team tools](https://uk.reuters.com/article/fireeye-cyber/us-cybersecurity-firm-fireeye-discloses-breach-theft-of-hacking-tools-idUKKBN28I34H). As a result of the breach, [FireEye released a ...

An interesting set of slides; the author uses [Symbolic Execution](https://en.wikipedia.org/wiki/Symbolic_execution) via [Klee](https://klee.github.io/) to model various aspects of routers and discover actual, exploitable bugs within routers.

I lead the Kubernetes audit, so if you have any questions I'd be happy to answer! You may also be interesting in [the GitHub repository we used to run the assessment](https://github.com/trailofbits/audit-kubernetes). Also interesting, /u/cji was on the Audit WG for Kubernetes, so you can *also* a...

> Maze solving algorithm implemented in sed There's also [the associated gist](https://gist.github.com/xsot/99a8a4304660916455ba2c2c774e623a) which looks really neat.

From the abstract: > We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and non-termination. > We propose Hoare Type Theory (HTT), which incorporates Hoare-style specifications into types, ...

Whilst the main focus is on Scala, the slides cover refinement types, capabilities, and so on, as applied to the work that normal programmers would have (like accepting client data from a web form.

From the abstract: > We are investigating a new approach to compiling Standard ML (SML) based on four key technologies: intensional polymorphism [23], nearly tag-free garbage col lection [12, 46, 34], conventional functional language optimization, and loop optimization. To explore the practicalit...

An interesting discussion of F# Data (at least for me, someone who only occasionally dives into F#), with some practical examples as applied to Web scraping.

> This essay uses Freedom Of Information Act (FOIA) documents to illustrate one of the earliest recorded remote operations against a major US Government agency. Special thanks to the employees of Los Alamos National Labs who were responsive to my FOIA request and even reached out after my initial th...

The [Google Cache](https://webcache.googleusercontent.com/search?q=cache:_K7OIiWrM6wJ:https://www.nerc.com/pa/rrm/ea/Lessons%2520Learned%2520Document%2520Library/20190901_Risks_Posed_by_Firewall_Firmware_Vulnerabilities.pdf+&cd=1&hl=en&ct=clnk&gl=us) of the NERC report (I'm posting the news article ...

From the Abstract: > Localizing type errors is challenging in languages with global type inference, as the type checker must make assumptions about what the programmer intended to do. We introduce Nate, a data-driven approach to error localization based on supervised learning. Nate analyzes a lar...

From the Abstract: > We present an approach for interactively visualizing static analyses built using the abstracting abstract machines (AAM) methodology—a process that yields a static program analysis by abstract interpretation of an abstract machine. The resulting analysis is a state graph of a...

This is a quick intro to SMT (specifically Z3) and its application to exploitation. I'm pretty interested in [Eclipser](https://github.com/SoftSec-KAIST/Eclipser), which we even [use a bit at work](https://blog.trailofbits.com/2019/05/31/fuzzing-unit-tests-with-deepstate-and-eclipser/), and things l...

"[Abstract]. This paper describes a verfied compiler for PreScheme, the implementation language for the vlisp run-time system. The compiler and proof were divided into three parts: A transformational front end that translates source text into a core language, a syntax-directed compiler that tran...

tl;dr: a discussion of language wars and [Programmer's Workbench Unix (PWB)](https://en.wikipedia.org/wiki/PWB/UNIX).

There's no "agda" or "plt" tags, so the above will do. This is an interesting pre-print on working with safe DSLs and the like in Agda. It looks neat, but I'll have to dive into it more later. The abstract: > Syntaxes with binding are omnipresent in Programming Languages research but also in...

Apparently improves the implementation of `^` in MLTon by quite a bit, but I thought it was a neat demo of using the MLTon FFI.

The video from my talk "Symbolically executing a fuzzy tyrant" [The slides are available on GitHub](https://github.com/lojikil/fuzzy-tyrant), as is [the tool that I talk about at the end](https://github.com/lojikil/uspno.9). It's more of a survey of things that I work with and am interested i...

An interesting article from SpecterOps on attacking Active Directory. From the article: > By applying the MS-RPRN abuse issue (previously reported to Microsoft Security Response Center by my workmate Lee Christensen) with various trust scenarios, we determined that administrators from one forest ...

Jerry does some interesting legwork here to check US CERT's release of data regarding the Russian infosec espionage (yes, I refuse to say the word "cyber"). I _kinda_ want to talk to him about doing some more, but I need to dig into the JAR data more myself first. Still, a neat read on what he found...