ammar2

They also come with a web browser that runs a full coding language, javascript.

The operating system is supposed treat end-applications like games and browsers as untrusted and provide isolation against them. The real kicker here is the bug in the `fs` service.

Here is the 2020-2024 Model Y manual's instructions on opening the back door with power loss, doesn't seem that obvious to me (you have to "remove the mat from the bottom of the rear door pocket" !): https://www.tesla.com/ownersmanual/2020_2024_modely/en_us/GU...

At least on the newer ones it looks like it at least has signage and is less obstructed: https://www.tesla.com/ownersmanual/modely/en_us/GUID-A7A60DC...

It's not that much of a stretch: give the LLM a top-level proposition for the thing you want to prove and have it hack away at it. Each sub-step is verified in lean so you know it's correct. But, the linked post definitely suggests otherwise.

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.

That assumes the natural language paper came first and then was formalized in lean. I haven't looked too deeply into how these labs solve these problems (or if they even specify this publicly) but you could also start with lean and then write the natural language proof based on it.

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.

The Xbox does not use AMD's Platform Security Processor, they have their own custom controller on die with Microsoft hardware and their own custom BootROM. This custom security processor actually has its own bit of RAM entirely in the die and doesn't even go out to the DRAM at all.

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

Not sure if it opens up that much on them as far as their security processors go. Modern consoles already treat DRAM as completely untrusted (an attacker could just sit on the DRAM bus and sniff/issue requests there).

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-...

Of note, even that 97% of original code that is now "safe in the rust sense" could violate invariants through safe blocks that cause memory-safety issues. I can't say exactly how the LLM-ported Rust code made use of unsafe but see https://www.ralfj.de/blog/2016/01/09/the-scope-of-unsafe.htm...

If you feel like increasing your power as per your post, this is a somewhat decent first LLVM issue, take a look at WebAssemblyCFGStackify.cpp :)

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!

Not sure if it's a stated goal somewhere official but there's been plenty of fixes of the years moving stuff to be deterministic, e.g https://github.com/llvm/llvm-project/commit/cdbde3aacc1260a7...

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.

The PS5 also runs apps (games/browser) under a hypervisor. There was a hypervisor escape though coupled with webkit as an entrypoint:

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

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

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

> GitHub runs a great program on HackerOne

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.

heh, a friend actually pointed out a typo on a first draft and said "maybe you shouldn't fix it to show it's not LLM written".

It's not just based on that, if you read the linked report from 2023 (https://blog.ammaraskar.com/vscode-rce/), I had a bug with the exact same impact of token exfiltration (It did need one additional click on the VSCode interface). They marked it as low severity, fixed it silently, didn't acknowledge that it had security impact and did not provide me any credit much less a bounty.

Update as of 3rd June: Microsoft has fixed this with a stopgap fix by adding a confirmation when opening notebooks in web VSCode and not allowing trusted publisher to be skipped by commands (https://github.com/microsoft/vscode/pull/319705).

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

You cannot, it doesn't go through the regular OAuth flow. GitHub just automatically grants it a token.

1 and 2 are correct, take a look at the PoC repo here: https://github.com/ammaraskar/github-dev-token-steal-poc/tre...

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.

Thank you, that's a very kind comment.

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.

> instead of clout

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.

> it'd be awesome if the in-browser IDE launched with a temporary per-repo permission scope

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...

Also, the Github enterprise code is "obfuscated" but it uses a trivially reversible method just meant to be a minor roadblock. After you get past that you get the full ruby source code, no minification or anything.

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.

Aah, the newlines were the thing I was missing. That makes sense then.

PEPs aren't necessarily just for language changes, e.g https://peps.python.org/pep-0436/ which is largely a CPython implementation detail.

Could you elaborate on this bit on why Github's secret masking doesn't work here:

> GitHub Actions' built-in secret masker matches registered values as exact substrings. When the exception message is rendered by Symfony Console it may wrap, embed in In BaseIO.php line N: framing, or interleave with ANSI control sequences. So the masker does not redact, and the plaintext token reaches the log.

What does this log rendering look like such that the token from that code snippet becomes interleaved enough to not be a substring match?

I'm not familiar with composer/Symfony but I would expect something like:

  Line 34: Foo bar
  Line 34: <red>Foo bar</red>

> (and agents)

Ironically, agents have the exact same class of problem.

> Microsoft would fork it within hours

I haven't trudged through Chromium's commit statistics but has Microsoft been upstreaming many contributions? I'm skeptical that they are ready to take on the full brunt of Chromium maintenance on a whim, it would take a decent while to build up the teams and expertise for it.

Glad this feature is built into most modern operating systems these days.

For MacOS (Sequoia+) you can just forget the network and reconnect to get a new MAC address [1].

Android's documentation for if it decides to generate a new address per connection is a little vague [2], but I'm guessing forgetting and reconnecting works as well, you may also need to flip the "Wi-Fi non-persistent MAC randomization" bit in developer settings.

On Windows, flipping the "Random hardware address" switch seems to cause it to generate a new seed/address for me.

[1] https://support.apple.com/en-euro/102509

[2] https://source.android.com/docs/core/connect/wifi-mac-random...

> it includes instructions for stack manipulation, binary operations

Your example contains some integer arithmetic, I'm curious if you've implemented any other Python data types like floats/strings/tuples yet. If you have, how does your ISA handle binary operations for two different types like `1 + 1.0`, is there some sort of dispatch table based on the types on the stack?

Aah, neat! Yeah, piggy-backing off pypy's work here would probably make the most sense.

It'll also be interesting to see how OP deals with things like dictionaries and lists.

> I'd prefer to move forward based on clear use cases

Taking the concrete example of the `struct` module as a use-case, I'm curious if you have a plan for it and similar modules. The tricky part of course is that it is implemented in C.

Would you have to rewrite those stdlib modules in pure python?

What you're proposing is reminiscent of Keybase's account verification system. You make a post or equivalent on each platform with cryptographic proof that it's you. (e.g here's mine for GitHub https://gist.github.com/ammaraskar/0f2714c46f796734efff7b2dd...).