A fork of rust-analyzer, called verus-analyzer, provides support for Verus syntax and actions (including new proof-specific actions) https://github.com/verus-lang/verus-analyzer/

This reminds me of a bugfix [1] I added to nmap almost a decade ago, where runtime interaction was previously broken due to interaction with sudo and signal propagation. Was a fun rabbit-hole to figure out why the issue was happening.

[1]: https://github.com/nmap/nmap/commit/f2e162d2245679f420b40feb...

I haven't had a chance to mess around with it much, but the coz-profiler [1] uses basically the same idea, but the other way around (i.e., slow down everything else to get a "virtual speedup") which helps quantify what the effect of optimizing some code would be.

I learnt about this tool from Emery Berger's talk [2] on this (at strangeloop), which I highly recommend. Lots of really nice insight, even outside of this tool.

[1] https://github.com/plasma-umass/coz [2] https://www.youtube.com/watch?v=r-TLSBdHe1A

Came to say the same thing, this Berger talk is phenomenal. I have watched it twice, planning on at least a third.

A fun read where the "could you still detect" portion turns out to be a very important plot point: Thrice Upon a Time by James P Hogan (https://www.goodreads.com/book/show/849488.Thrice_Upon_a_Tim...)

Relevant (and super cool) previous work, done by Orange Tsai: https://www.blackhat.com/docs/us-17/thursday/us-17-Tsai-A-Ne...

Hi! Author here. Happy to answer any questions.

Reader mode should be working now. Just tested on mobile Safari.

Hi! It looks like I'd forgotten to update the CSS in one portion, due to this, on medium-sized screens, there was an overlap that occurred. This should be fixed now.

As per the full contest rules (https://www.zerodayinitiative.com/Pwn2Own2019Rules.html):

> If more than one contestant registers for a given category, the order of the contestants will be drawn at random. Based on the contestant order, the first contestant will be given an opportunity to attempt to compromise the selected target. If unsuccessful, the next randomly drawn contestant will be given an opportunity. This will continue until a contestant successfully compromises the target. The first contestant to successfully compromise a selected target will win the prize money for that target in that category. After a target has been compromised, the contest for that category is over and no other contestants will participate in the contest for that category (unless Sponsor has offered an additional winner option, which would be announced at the conference if applicable).

Your whitelisting is quite good!

I still haven't been able to do complete code execution yet, but have reasons to believe it might be possible.

Simply using `x1` as input causes it to print "deadbeef11 is not defined". Additionally, parens are allowed, and there is the `=>` arrow syntax for defining functions. Thus, we have a way to define variables, a way to define lambda abstractions, as well as a way to perform applications. Therefore, we have the untyped lambda calculus. This is Turing complete, so I have reason to believe that it should be possible to execute arbitrary code. I just need to find some time to do so :)

Update: `(x1=>x1(x1))(x1=>x1(x1))` gives "Too much recursion" :D