There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code