• 0 Posts
  • 21 Comments
Joined 2 months ago
Cake day: September 5th, 2026
  • borosilicate@lemmy.dbzer0.comtoTechnology@beehaw.org•Some iPhone Duo displays are cracking, seemingly all in the same way
    7·
    4 days ago

    My best friend has has had the Samsung version of this for four different generations now. I’ve always been a hater about it but now in gen 4, there are very few issues with Samsung’s folding phones… but they still suck and are fragile as hell.
    My conclusion: all folding screen phones like this are shite and Apple gets a first generation mulligan on this one. This release is as bad as any in their history and they should have seen it coming a mile away given Samsung’s myriad issues.

    My rule: NEVER BUY AN OVERPRICED, GIMMICKY, FIRST-GENERATION APPLE PRODUCT.

  • borosilicate@lemmy.dbzer0.comtoRust@programming.dev•Signal Protocol in Rust
    31·
    6 days ago

    I used a frontier model to generate an allium spec from your repo and it found a few bugs. I like to run apps through allium to prepare for formal verification because it tends to find a LOT of flaws in even the most robust apps. The allium spec file is too large to share here but it can be generated by any frontier model.

    Defects, three of them confirmed by running probes against the crate:

    • P1, a late message from the previous chain breaks the session. The decrypt code never keeps the leftover keys of the old receiving chain, and it reads the header’s previous chain length only as associated data. So a delayed message from the old chain looks like a new ratchet key. The session steps the ratchet again and the tag fails. In the probe, the next good message also failed with an AES-GCM error. Signal handles exactly this case, and the crate’s out-of-order test only reorders messages within one chain.
    • P2, one forged message with a made-up ratchet key desyncs the session for good. The ratchet step and key skipping happen before the tag is checked, and they’re never rolled back. In the probe, the next real message failed.
    • P3, a forged message naming a skipped key deletes that key before the tag check. The real message then fails with “Message number mismatch”.
    • The signed prekey’s signature is never checked. x3dh_initiate_internal doesn’t call verify_signed_prekey, and the WASM API doesn’t expose it. Prekey authentication depends on every application remembering to do it.
    • The X3DH associated data isn’t bound to the two identities. It’s the constant “X3DH_Key_Exchange” rather than both identity keys, and the ratchet never uses it anyway.
    • The identity key and the signing key are unrelated. It uses a separate, unbound Ed25519 signing key instead of XEdDSA on the identity key.
    • The first chain gets no DH ratchet. On both sides it’s derived from the X3DH secret alone.
    • Smaller issues:
      • There’s no cap on the total number of skipped keys.
      • Cleanup drops keys in string order, not oldest first.
      • The send counter is a u32 with no overflow check.
      • The DH output isn’t checked for all-zero values from small-order keys.
      • The legacy encrypt_message helper returns the message key to JavaScript. Variants, not defects: the non-standard HKDF salts and info strings. Both sides agree on them, and the spec says so.
    -- VIOLATED: only one decrypt's skip is capped (max_skip); nothing caps
-- the total unless the application calls cleanup, so a peer that keeps
-- skipping grows the state without limit.
invariant SkippedKeysAreBounded {
    for s in Sessions:
        s.skipped.count <= config.max_skipped_total
}

invariant OneTimePreKeysBelongToOneSession {
    for a in Handshakes:
        for b in Handshakes:
            a != b and a.one_time_prekey != null
                implies a.one_time_prekey != b.one_time_prekey
}

invariant ResponderCannotSendBeforeReceiving {
    for s in Sessions:
        s.role = responder and s.receiving_ratchet_public = null
            implies s.sending_chain_key = null
}

open question "Should x3dh_initiate_internal take the signing key and signature and verify the signed prekey itself, so a caller cannot skip it?"

open question "Should the identity key sign with XEdDSA, so there is one long-term key instead of an unbound X25519 and Ed25519 pair?"

open question "Should decrypt work on a copy of the state and commit only after the tag verifies?"

open question "Should the associated data be IK_A || IK_B and be passed into every seal and open?"