skybrian's recent activity

  1. Comment on Looking for advice: How do I find out what stocks to invest into? in ~finance

    skybrian
    Link Parent
    Saying it's two people simplifies things. It needs to be enough investors with enough money to change the price despite other investors having different opinions. And from the outside, prices are...

    Saying it's two people simplifies things. It needs to be enough investors with enough money to change the price despite other investors having different opinions.

    And from the outside, prices are opaque. They can be badly wrong, and you can rarely tell the difference between a well-informed market and one that's about to be blindsided by something unexpected.

    It's a lot easier to see that a market price was wrong after the news happened.

  2. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    Yeah, who knows. Depending on what happens in the elections for the Senate, Trump might not get any more Supreme Court appointments even if there's a vacancy.

    Yeah, who knows. Depending on what happens in the elections for the Senate, Trump might not get any more Supreme Court appointments even if there's a vacancy.

  3. Comment on LLMs are making formal software verification feasible at a much larger scale in ~comp

    skybrian
    Link
    This is potentially very good news for cybersecurity. For example, today things like video codecs and font renderers are a common source of vulnerabilities. It may be practical before too long for...

    This is potentially very good news for cybersecurity. For example, today things like video codecs and font renderers are a common source of vulnerabilities. It may be practical before too long for browser vendors, at least, to use fuzz tests and AI to prove that their codecs have no security bugs, and then attackers would have to look for things like OS bugs or hardware glitches.

    If that happens, it will be at least as important as Rust is for memory safety.

    Eventually, after AI has been optimized for this and there are suitable software packages available that implement it, ordinary software engineers will be able to run AI on their fuzz tests overnight to prove that a new release is free of many classes of security bugs.

    And if you don't do that, attackers probably will, because it will find any security bugs that exist.

    I was rather skeptical about how important formal verification would be for software, but if it can be almost fully automated, it will become essential. You don't need to know a lot of math to write fuzz tests.

    1 vote

  4. Comment on Meta ordered to pay $25 billion penalty in New Mexico Cambridge Analytica case in ~tech

    skybrian
    Link Parent
    An exec saying they're confident they will win in appeal isn't a factual claim, and just in case, there is usually a legal disclaimer about forward-looking statements, too.

    An exec saying they're confident they will win in appeal isn't a factual claim, and just in case, there is usually a legal disclaimer about forward-looking statements, too.

    10 votes

  5. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    (edited )
    Link Parent
    That change required appointing new judges to the Supreme Court, though. Time is running out for Trump to do more of that. And overturning Roe vs. Wade took 49 years, so that's more of an example...

    That change required appointing new judges to the Supreme Court, though. Time is running out for Trump to do more of that. And overturning Roe vs. Wade took 49 years, so that's more of an example of how difficult it is.

    I make no claim that this is impossible, given enough time, but the Republicans will need to win more presidential elections, which makes it not an immediate threat.

  6. Comment on LLMs are making formal software verification feasible at a much larger scale in ~comp

    skybrian
    Link
    From the article: [...] [...] [...] [...] [...] [...] [...]

    From the article:

    For this project, we started with fuzz tests. In these tests, developers write an entry point2 into their code that takes inputs, such that any input that causes a crash is a bug the authors care about. Then the fuzzer, a testing engine, generates enormous numbers of semirandom and mutated inputs at the entry point to try to find a bug (visualized in Figure 1). The longer a fuzzer runs, the more bugs it can find. But this is inherently a brute-force process, with no guarantee of exercising every possible code path, regardless of how many inputs you try.

    [...]

    To find all the bugs that would’ve been surfaced by a fuzz test, we turned the fuzz test into a spec defined over the compiled RISC-V instructions. The spec says that the fuzz test won’t crash for any input less than 64 MB.3 If Claude can prove this spec, the fuzz test on RISC-V becomes superfluous: fuzzing that entry point will never find any bugs.

    We did this for hundreds of projects in Google’s OSS-Fuzz initiative, which provides continuous fuzz testing for qualifying open-source projects. OSS-Fuzz contains thousands of developer-authored entry points that look for broken code properties by crashing (for example, on a failed assertion). OSS-Fuzz automatically instruments C and C++ programs with AddressSanitizer4 (ASan), causing them to crash whenever memory is accessed improperly (which is a leading cause of software vulnerabilities). Broad-spectrum specifications like memory safety apply to almost all software.

    [...]

    Over the span of a few weeks, Claude successfully patched the bugs it found and then proved that there are no crashes on any input (up to 64 MB) for 239 entry points across 123 different OSS-Fuzz libraries. These proofs operate on the compiled RISC-V instructions (i.e., executable binaries), and they comprise about 180 million lines of Rocq, with a typical proof running to about 600,000 lines to provide security guarantees on binaries with a median length of 18,000 RISC-V instructions. These proofs are built by translating the RISC-V assembly code to a mathematical model using Theorem’s RISC-V instruction and Linux process semantics. This means these proofs currently assume that the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux OS. Expanding the scope of these proofs is well within reach, as it would involve standardizing semantics for more assembly architectures and other operating system processes. See an expert’s take on the proofs Claude wrote.

    [...]

    This doesn’t mean these libraries contain no bugs. Instead, it means that any remaining bugs either are to be found within the artifacts listed above or are outside the scope of Claude’s proof. Hardening those still-possibly-buggy trusted components (Rocq, RISC-V, and Linux semantics) is not insignificant, but it’s a far more tractable task than debugging every line of code the scaled-out proofs cover—especially as this approach can secure an arbitrary number of projects without increasing the size of the trusted components.

    [...]

    Many of the bugs we found are ones that a fuzzer would be unlikely to ever find. Fuzzers mutate small inputs, typically capped at 1 MB, and typically rely on code coverage to guide them toward bugs. While proving an entry point in one library, Claude found a counter underflow in its copy of a decompressor that led to an out-of-bounds write, but only on inputs of around 20 MB that had one rare, specific layout. Other bugs include an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory, an out-of-bounds read in another library that needed a particular sequence of calls across two handles to the same file, and a rediscovery of CVE-2026-56132 in libexpat, which needed deeply nested input. Claude also found logic bugs that never crash at all. While proving that one library was memory-safe, for example, it noticed that a feature for restricting which files an application can load isn’t always enforced.

    [...]

    Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.

    This can also occur even when the properties are not directly specified by the developer. For example, in order for Claude to complete its OSS-Fuzz proof for cpp-httplib, it was necessary to rule out the possibility of a stack overflow due to too much recursion in the std::set destructor. This recursion depth is bounded by the maximum depth of a tree, so Claude had to prove (on machine code!) that libc++’s red-black tree rebalancing algorithm is correctly optimized to keep the tree’s depth logarithmically bounded.

    [...]

    In another experiment, we asked Claude to develop an interpreter for a large subset of Python in Rust, and to prove (using Verus, a verification tool for Rust) that it adheres to the CPython semantics outlined in an academic paper. We then measured the adherence to CPython’s behavior empirically, running over 1.7 million randomly generated Python programs, finding identical behavior with CPython in 99.95% of tests, with remaining test differences as unsurprising known corner cases.

    We also found issues in several widely used and critical applications via formal verification attempts of simple security properties. In one of them, we discovered a previously unknown logic bug that had been latent for more than a decade. During an effort to verify a widely used PDF reader, we found as many security bugs in one week as are typically reported in a year.

    [...]

    This reusability of proofs is how Mathlib, a shared library of formal mathematics in Lean, grew to nearly 300,000 theorems submitted by over 700 contributors: each new proof builds on the existing body of work. We accumulated a similar body of proofs in the course of our OSS-Fuzz effort, some of which we’re including in our release (we are not releasing proofs that may reveal an unpatched bug in the open-source software).

    1 vote

  8. Comment on Offbeat Fridays – The thread where offbeat headlines become front page news in ~news

    skybrian
    Link
    Meet the Guy Who Excavated O’Hare’s 50-Ton Boulder From the article: [...] [...] [...] [...]

    Meet the Guy Who Excavated O’Hare’s 50-Ton Boulder

    From the article:

    Ron Pitelka has an idea for what to name the 50-ton prehistoric boulder that was unearthed this summer at O’Hare Airport.

    “I would probably call it ‘Geo,’” Pitelka said. “It might not be funny, but it’s a little more appropriate.”

    [...]

    In all of the 23 years he’s been operating excavators — so, half his life — “I’ve never seen a boulder this big come out of the ground. It’s pretty damned rare,” Pitelka, who lives in Homer Glen, told WTTW News. “I was like a kid on Christmas.”

    [...]

    Pitelka’s colleague, Matt Tracy, attempted to budge the object with his bulldozer. It didn’t move. Pitelka tried to hook it and the Cat 352 balked. Eventually, with the combined force of the bulldozer pushing and the excavator pulling, they got the boulder out of the ground.

    [...]

    Over the years, Pitelka has rescued some of these rocks and deposited them at his mom’s five-acre property, including a large hunk of limestone that, when he dumped it out of his truck, split in half to reveal a perfect trilobite fossil, convex on one side and a matching imprint on the other.

    “I’m always looking for stuff like that,” he said. “When I go on vacation, I always bring a rock back.”

    [...]

    Knowing that the massive find at O’Hare could easily be 300 to 400 million years old, Pitelka asked the construction superintendent to fight for the behemoth’s preservation. He hoped maybe it could be embedded in the basin’s embankment, where he could view it via Google earth.

    It was only this week, when the airport announced the naming contest for the rock, that Pitelka learned the boulder had been saved and was destined for greater things.

    “I was so excited to hear that the right people got involved,” he said. “I’m absolutely ecstatic it’s going to be on display. For me, as an (excavator) who loves boulders, it’s the coolest thing that people understand its historical significance and appreciate it.”

    5 votes

  9. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    No, the idea that it would happen that way, where we would wake up surprised by the election results that are obviously a fraud, is still magical thinking. Voting is very decentralized. Their...

    No, the idea that it would happen that way, where we would wake up surprised by the election results that are obviously a fraud, is still magical thinking. Voting is very decentralized. Their attempts would take time, and would be reported on. They have been reported on.

    3 votes

  10. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    (edited )
    Link Parent
    Yes, of course it's a serious concern, as an immigration issue and a civil rights issue, but it's not going to affect the elections. (Other than as a campaign issue.)

    Yes, of course it's a serious concern, as an immigration issue and a civil rights issue, but it's not going to affect the elections. (Other than as a campaign issue.)

    1 vote

  11. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    Yes, they will keep trying, but they're still not Lex Luthor. Overturning a Supreme Court ruling isn't a matter of getting more lawyers involved. A prediction with a "magic happens here" step in...

    Yes, they will keep trying, but they're still not Lex Luthor. Overturning a Supreme Court ruling isn't a matter of getting more lawyers involved. A prediction with a "magic happens here" step in the middle isn't very credible, and by spreading FUD you're acting as the Trump administration's dupe. They can't stop enough people from voting to matter, so they're going to try to scare them away instead. Why help?

    7 votes

  12. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    Certainly the Trump administration has tried in many ways. But you are not more clear. Did not happen! The Supreme Court ruled against them. They're still trying, but they keep failing. And even...

    Certainly the Trump administration has tried in many ways. But you are not more clear.

    Revoking birthright citizenship

    Did not happen! The Supreme Court ruled against them. They're still trying, but they keep failing.

    And even if it did happen, it wouldn't effect the elections for long after Trump is gone, because babies don't vote!

    So why bring it up? Why are you muddying the waters? Why are you trying to make Trump seem ten feet tall? Whose side are you really on?

    7 votes

  13. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    It is, though. This is terrible, but it's unlikely to affect the elections. Please vote. And don't discourage people from voting! That's just making it worse.

    "You'll never have to vote again" wasn't hyperbole.

    It is, though. This is terrible, but it's unlikely to affect the elections. Please vote. And don't discourage people from voting! That's just making it worse.

    10 votes

  14. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

    skybrian
    (edited )
    Link Parent
    If one person experiences it, it's a real issue. But there is a difference in logic between #MeToo and #YesAll tags. #YesAll tags are making a much stronger claim. Not just that you experienced...

    If one person experiences it, it's a real issue. But there is a difference in logic between #MeToo and #YesAll tags. #YesAll tags are making a much stronger claim. Not just that you experienced it, or that the experience is common, but that "everyone" experiences it. This is not just about yourself. It's denying the lived experiences of strangers that you have no right to speak for. It's denying that the world is a diverse place and people have different experiences. It's saying that no, actually, things are the same everywhere. Who has the right to make such a claim from personal experience?

    As a matter of logic, saying that "everyone" experiences something actually is refuted by someone saying, "well I don't see it." #YesAll a very strong claim, often easily disproved.

    Though of course, people are not computer programs and often we say things that aren't meant literally. The meaning of a term in context could be something else entirely.

    A charitable way to understand #YesAll is to assume that it's not what they really meant. But the term itself argues for being taken literally. It's effectively saying "I meant what I said."

    So, if you don't want that meaning, maybe avoid using "YesAll" hashtags?

    10 votes

  15. Comment on eMudhra intermediate CA compromise in ~tech

  16. Comment on PHP warns it plans to release two emergency patches imminently in ~comp

    skybrian
    Link Parent
    Here is Calif’s page on the bug:

    Here is Calif’s page on the bug:

    No special harness, or access to models that weren't generally available to everyone were used in the initial bug discovery. I focused on something I had a background in, knew its vulnerability history well, and held a theory that specific bugs lurk within the codebase. This shows that "know your target" is still as applicable as ever, even in the LLM dominated VR age. No model is simply capable of unearthing "all bugs" with simple prompts. At least for now.

    There are some practical research implications here. LLMs may have ingested public historical vuln data, but in their default variant analysis tends to move from the newest and most prominent bugs toward nearby older code. They do not reliably begin with obscure twenty-year-old exploitation primitives. Keeping your own mental catalog of a target's vulnerability history lets you prompt that direction explicitly.

    5 votes

  17. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

  18. Comment on PHP warns it plans to release two emergency patches imminently in ~comp

    skybrian
    Link
    And yep, these bugs were found via AI. From the Wiz blog: ... ... And if they didn't find it, apparently someone else would have? From OpenAI's blog: (Calif is apparently a security firm.)

    And yep, these bugs were found via AI.

    From the Wiz blog:

    In this post, we explain how frontier AI helped us find and fix vulnerabilities that had remained hidden in the PHP codebase for more than a decade. The issues described below all stem from key architecture decisions, some made over a decade ago, and were grouped under two CVEs, with severity reaching CVSS 9.2. The work grew into a cross-industry effort to protect customers, find variants, deploy detections and mitigations, and verify a patch in time for coordinated disclosure.

    ...

    We believe PHP2Shell could mark a similar turning point for the AI era, illustrating how AI can change the practical exploitability of longstanding vulnerabilities. Building the exploit required chaining multiple flaws and adapting to each target’s memory layout through repeated testing and debugging. Frontier models were critical to making this process practical, enabling us to develop and adapt working exploits across multiple applications in hours. As the time and expertise required for this work decrease, complexity may no longer provide a meaningful barrier, changing how we define what is vulnerable in practice.

    ...

    We used Wiz Atlas, Gemini 4 Argon and GPT-5.6 Sol throughout this research. Notably, Gemini 4 Argon made an invaluable contribution to finding the vulnerability, exploit development, attack detection, and validation of the patch.

    And if they didn't find it, apparently someone else would have? From OpenAI's blog:

    Calif identified a critical flaw using GPT‑5.6 Sol as part of our Patch the Planet initiative, with Wiz also independently discovering and reporting both vulnerabilities

    (Calif is apparently a security firm.)

    2 votes

  19. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

    skybrian
    Link Parent
    I doubt anyone post links here because they they think they’re bait. They post them because they agree with them or at least think they’re interesting. But writing style can be contagious and...

    I doubt anyone post links here because they they think they’re bait. They post them because they agree with them or at least think they’re interesting. But writing style can be contagious and “interesting” links are sometimes originally from influencers or people writing in a similar style, because it seems catchy. It might not seem objectionable when you’re on the same side.

    8 votes

  20. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

    skybrian
    Link Parent
    It’s true that we are responsible for our own posts and our own replies. But also true that we are asked to try to think about how others might respond. When starting a topic, there is this...

    It’s true that we are responsible for our own posts and our own replies. But also true that we are asked to try to think about how others might respond. When starting a topic, there is this boilerplate:

    Please post topics that are interesting, informative, or have the potential to start a good discussion.

    What would a good discussion look like? Sometimes you can post something along with a link that tries to head things in a good direction.

    It doesn’t always work and it can be taken too far so you don’t post at all. I think there’s a middle ground?

    There’s also a common impulse to try to influence what other people post. That’s what this topic about, right? It’s yet another discussion of what should be okay to post. We have no control over what other people do, but sometimes we try to influence them.

    5 votes