That is definitely interesting because how do you know the 88 hours of work are correct before you throw another 17 hours of lean formalization work on it? You could end up just finding out there was some hallucination in the original work.

For what it's worth the initial lean specifications for the top-level theorems generally come from human written formalizations such as in https://github.com/leanprover-community/mathlib4/blob/021ce6... so we can be reasonably confident about their correctness.

See the slide on Tony Chen's presentation about Xbox One security https://youtu.be/U7VwtOrwceo?t=843 and this video from the person who hacked the Xbox One https://youtu.be/FTFn4UZsA5U?t=299

The Xbox One for example encrypts all the DRAM it uses after it gets out of the main CPU die. See this part of Tony Chen's presentation https://youtu.be/U7VwtOrwceo?t=956

Also see this bit on the Apple Secure Enclave in the "Memory Protection Engine" section which also explains how they encrypt stuff stored in DRAM: https://support.apple.com/guide/security/the-secure-enclave-...

llvm/test/CodeGen/WebAssembly/cfg-stackify-eh.ll and friends are existing tests that you can kinda mangle if you want to get a good reproducer.

Also take a look at https://discourse.llvm.org/t/reverse-iteration-bots/72224

Otherwise, happy to put my reproducer/patch on the bug after you file it!

The internal programming guide also says which collections to use for deterministic iteration order: https://llvm.org/docs/ProgrammersManual.html#llvm-adt-setvec...

So definitely a bug here.

* https://ps5dev.github.io/ps5-wiki/hypervisor

* https://github.com/PS5Dev/Byepervisor

* https://github.com/PS5Dev/PS5-UMTX-Jailbreak/blob/main/READM...

I agree, for the record here's my HackerOne profile https://hackerone.com/ammar2/hacktivity?type=user

Just for context, that 2023 bug was initially reported to GitHub's HackerOne program and they explicitly told me it was out of scope for them and to take it to MSRC:

> We have reviewed the report and determined that the vulnerabilities is in VS code and the fix will be implemented by Microsoft. As a result, it is not eligible for reward under the Bug Bounty program. Please follow-up with Microsoft via the report you submitted.

There was also an additional bug that allowed an attacker to exfiltrate private repo contents with a github.dev link that MSRC also marked as not having security impact.

I absolutely loved working with GitHub folks on the GitHub bug bounty program, they're responsive, go into technical details with you and are awesome to deal with. MSRC is like the polar opposite of that.

That's probably one of the fastest responses I've seen from a vendor.

We can try to just put a `my-extension/extension.js` for the most direct execution but the CSP blocks that. It's only a script-src CSP blocking it though, so fetching the package.json is still kosher. So we end up using it to contribute a keybinding instead.

I have no interest in selling these vulnerabilities or sitting on them. At the same time, it feels really bad to have a vendor disrespect the hours it can take to make a proof-of-concept by just patching it silently and not crediting you or acknowledging it.

I'm catching up on the infosec twitter side but it seems like it was even worse. A lot of people have the same story as me in 2023 of "they silently patch the bug and don't even credit you" which really stinks.

That's actually exactly what they do for codespaces. The token only has read/write on the repo you activated for the codespace [1]. They should definitely consider doing that for github.dev as well.

[1] https://orca.security/resources/blog/hacking-github-codespac...

Comments URL: https://news.ycombinator.com/item?id=48371562

Points: 660

# Comments: 101

For a while the key was literally:

> This obfuscation is intended to discourage GitHub Enterprise customers from making modifications to the VM. We know this 'encryption' is easily broken.