05. February 2019

Terminfo and its DSL

Programs for Linux that run in the terminal often use color. There are a few approaches to making this work. Many programs use hardcoded ANSI compatible escape sequences, which are widespread enough today that they work almost everywhere. There are drawbacks to hardcoding these and for that reason there’s a database called terminfo, which has its own stack-based Domain Specific Language (DSL).


06. January 2019

Alignment Checking & Meltdown

Here is some interesting news for compiler writers worried about Meltdown. I have previously described a way to get hardware-based type checks (think branchless car, cdr, vector-ref, etc.) using alignment checks. It now appears that this technique may be immune to Meltdown-type attacks:

Alignment Faults.

Upon detecting an unaligned memory operand, the processor can (optionally) generate an alignment check exception (#AC). We found that the results of unaligned memory accesses never reach the transient execution. We suspect that this is because #AC is generated early-on (even before the operand’s virtual address is translated to a physical one). Thus, Meltdown-AC is not possible.

A Systematic Evaluation of Transient Execution Attacks and Defenses (2018, Canella, et al.)

The kernel unfortunately can’t use it because #AC does not work at CPL=0, but for user space it could be a great way to avoid some Meltdown vulnerabilities.

18. November 2018

Design Your Low-Bit Tagging with Z3Py

Low-bit tagging is a technique where the low bits of values are used to store type information. There are numerous benefits that come with this technique and it is quite popular in implementations of Scheme, JavaScript and other languages. But once you start down the road of bit-twiddling it is hard to stop and the design of the tagging system may become difficult to understand. So that’s when you look in your tool box and pull out something like Z3, which this article explores.