Dan Pittman

Engineer and Mathematician
published: 2023-03-08 | generated: 2024-10-16 | tagged: ,

(contact info available by downloading a pdf version of this document)

Intel Corporation

Technical Lead, Cryptography

08/2023 - Present

  • Ported OpenSSL AVX-512 RSA Implementation to AWS-LC and BoringSSL
  • Optimized AVX-512 XTS implementation to use on-stack keys in AWS-LC
  • Ported that optimized XTS implementation to OpenSSL (in progress)
  • Mechanical assembly dialect translation (in progress)

Technologies Involved

  • C, C++, GAS/Perl assembly (perlasm)
  • Haskell (asm translation)
  • Extensive mathematical optimizations involved in the RSA algorithm

Technical Lead, Hyperscaler Resource Management

10/2021 - 08/2023

We did weird and innovative Linux things that I can’t really talk about, both in the kernel and in userspace, to serve Intel’s hyper-scale customers.

Technologies Involved

  • C/Rust
  • Userspace page faults
  • OoT Kernel Modules
  • Linux’s virtual file systems (think cgroups’ filesystem)
  • Intel’s RDT
  • Intel’s top-down µarch PMUs, used in real time

Auxon Corporation

Principal and Founding Engineer

07/2018 - 10/2021

For the first half of my time at Auxon, I continued my exploration into applying proof theoretical methods for checking software at both compile time and runtime.

Once Auxon moved on from developing high-assurance software itself, I began focussing on the customer-facing edges of our product, finding that putting myself in the shoes of potential users came naturally. During this time I developed and implemented Modality’s log, check, and cumulative report features.

Additional Accomplishments

  • We made a runtime in Rust on top of seL4. In this runtime, we went through great lengths to extend the guarantees that seL4 provides to also be checkable at compile-time through techniques which can be summarized as “type-level programming”.
  • I owned the architecture-agnostic implementation for that runtime that used type-level induction to provide a mechanism for architecture-agnostic memory hierarchies.
  • I designed and implemented a memory-mapped registers library that provided:
    • Compile-type checked writes (for values known a priori).
    • A proof-carrying approach for runtime checking.
    • Complete proofs of that library’s correctness in Agda.
  • I built a tool in Haskell that translates Rust types (and therefore type-level programs) to Agda. I spoke about an early iteration of this at Strange Loop 2018.

Polysync

Principal Engineer

11/2017 - 07/2018

I came to PolySync to contribute to the high-assurance automotive runtime they were building working as a hybrid proof / software engineer. PolySync intended to use my work and research to find ways to blur the line between proof and program to instill further confidence in the integrity of the software they developed.

Additional Accomplishments

  • We made a toolchain for writing seL4 tasks in Rust.
  • I designed a distributed system whose core logic was session types predicated on Atkey-style indexed monads translated to Rust to run on seL4.

Intel

Sr. Cloud Software Engineer

12/2014-11/2017

  • I led a team that built a distributed execution engine that tried to model the data center as a category—states as objects, transitions as morphisms (ask me more about this, it was fun).
  • I worked on making persistent memory useful in cloud environments (Go/etcd)
  • I helped design and build a modular and flexible telemetry system for use in the data center.

VMware

Sr. Member of Technical Staff

12/2012-12/2014

  • I was one of the first 10 developers working on VMware’s public cloud platform, vCHS.
  • We made a globally distributed system which could deploy complete private VMware environments to the cloud in minutes. It did this through a number of interesting technologies including but not limited to: CQRS & Event Sourcing, AMQP, Cassandra, (and all of its finicky eventual consistency idiosyncrasies), and a homegrown Paxos implementation—which I was later responsible for replacing with Zookeeper.

Enterhost / Consuro

System Administrator

2/2012-12/2012

At Enterhost, a hosting provider, and its MSP arm Consuro, I was responsible for designing and then implementing and/or installing medium-sized networks involving VMware infrastructure, typically on customer premises with disaster recovery environments collocated at Enterhost’s datacenter.

WM Automotive

System Administrator

7/2008-2/2012

I was the primary IT provider for a midsize enterprise—an aftermarket automotive parts distributor and retailer. During the time I was there, I rebuilt their technology infrastructure from the ground up.

This included: * A network overhaul to include company-owned stores on the LAN. * Virtualizing the CRM/ERP software stack for the B2B arm of the business. * The deployment of Windows’ enterprise stack (Exchange / Active Directory), desktop imaging and deployment. * Centralized SAN-based storage. * An active/passive disaster recovery plan.