diff --git a/src/grants/nlnet-first.md b/src/grants/nlnet-first.md index f4003c1..e76cf45 100644 --- a/src/grants/nlnet-first.md +++ b/src/grants/nlnet-first.md @@ -30,13 +30,13 @@ TODO, come up with estimated budgets. ## Compare with existing/historical efforts -# UPEC, as described in "An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors" +### UPEC, as described in "An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors" According to , UPEC is limited in that it only works on a specific conservative mechanism (preventing speculative load instructions from executing untill all prior branches are resolved). Jacob Lifshay's idea, by contrast, should work even if the CPU runs speculative loads before resolving branches, with much less stringient conditions on those loads. -# "RTL Verification for Secure Speculation Using Contract Shadow Logic" +### "RTL Verification for Secure Speculation Using Contract Shadow Logic"