Research Scientist with a focus on memory management architectures for security.
MS, PhD, and Postdoc in Computer Science, 2012
University of Illinois at Urbana-Champaign
BS in Computer Science, 2005
University of Wisconsin-Eau Claire
I define and evaluate innovative security architectures for mitigating exploits and malware. I draw on my expertise in architecture, compilers, operating systems, virtualization, HW/SW co-design, and formal methods to effectively devise solutions that are well-adapted to workload requirements.
Principal Investigator for Intel’s project in the DARPA HARDEN program.
Served as Intel lead liaison for the SRC JUMP CONIX research center.
Advisor: Carl A. Gunter
National Defense Science and Engineering Graduate (NDSEG) Fellow
PhD Dissertation: Compact Integrity-Aware Architectures
MS Thesis: Dependable Emergency-Response Networking Based on Retaskable Network Infrastructures
TA for Advanced Computer Security (Instructor: Carl A. Gunter)
TA for Advanced Operating Systems (Instructor: Samuel T. King)
We developed a Network-on-Chip (NoC) firewall in Bluespec SystemVerilog configured by a dedicated core, and we demonstrated how it can enforce isolation between two instances of Linux on separate cores. We developed a shallow embedding of a subset of Bluespec into Maude, since both languages are based on term rewriting systems, and we used a Maude model of the NoC firewall to precisely identify a subtle vulnerability.
Extended a processor core written in VHDL with hardware support for detecting attempts to execute unverified code. Developed an integrity kernel and network server to enforce code whitelisting using processor extensions. Evaluated using an FPGA.
Published patent applications:
App, kernel, and hypervisor development for Linux, Windows, and embedded systems with Boost and generics experience
SAT/SMT solver (completed Coursera course)
Somewhat familiar with assembly language for other architectures as well
High-Level Synthesis (HLS) language based on Term-Rewriting Systems
Model checker based on Term-Rewriting Systems and Linear-Temporal Logic
Interactive theorem prover
Experience using Intel Quartus and Xilinx Vivado FPGA toolchains. Experience using Synopsys VCS and Mentor Graphics Modelsim simulators. Experience extending and maintaining an in-house Verilog simulator during an internship with Cray, Inc.
Logic programming language
Professional society memberships:
Conference and workshop reviews:
Selected Mentoring Experiences:
For messages related to my work at Intel, please contact me at michael dot lemay at intel dot com.
For other messages, please contact me at m at lemays dot org.
I post a mix of professional content and personal content on my website, and I categorize my posts accordingly. Separate RSS/Atom feeds are generated for each of those categories, and there is also a combined feed: