Hacker News

Top stories

Live mirror
30 storiesupdated just nowView source snapshot
  1. Goodbye Google (ocallahan.org)
    45comments
  2. F-Droid 2.0 (f-droid.org)
    288comments
  3. Show HN: Make cursed fonts like Times New Bastard (mitpit.com)
    80comments
  4. Show HN: Whiteboard (YC W26) – An open-source IDE for thoughtful software design (github.com/devdotfast)
    97comments
  5. Why is the liver so weirdly regenerative? (dynomight.substack.com)
    178comments
  6. 2DWillNeverDie (2dwillneverdie.com)
    23comments
  7. Fearless SIMD v1.0 (linebender.org)
    34comments
  8. Rails World 2026 Opening Keynote [video] (youtube.com)
    318comments
  9. Toyota is taking the Corolla electric (electrek.co)
    468comments
  10. My weird new hobby: Wandering around Tokyo on Google Maps (ahmedhossamdev.com)
    123comments
  11. Using LLMs to trace alchemical knowledge and decode 17th century letters (resobscura.substack.com)
    19comments
  12. Google’s Project Suncatcher to put ML infrastructure in space (blog.google)
    292comments
  13. Two-tier encryption in the UK (macanorak.com)
    384comments
  14. Writing Parquet files using Haskell (datahaskell.org)
    3comments
  15. Book review: Is parallel programming hard, and, if so, what can you do about it? (ahelwer.ca)
    33comments
  16. Opus 5.5 is good at explainer videos (launchvideo.io)
    110comments
  17. The Board Game of the Alpha Nerds (2014) (grantland.com)
    26comments
  18. Show HN: Air-gapped file encryption as self-decrypting HTML page (apeleg.com)
    17comments
  19. Security auditing in the age of (good enough) AI (trailofbits.com)
    12comments
  20. California is chasing wealth that has feet (landeconomics.org)
    569comments
  21. Sourcehut account takeover via build logs (XSS in ansi2html) (blog.arusekk.pl)
    17comments
  22. The forgotten battle of East Lansing (eastlansinginfo.news)
    15comments
  23. Show HN: Koi.rest – watch some fish and regain your balance (koi.rest)
    41comments
  24. WaveDigger: Dig into wireless signals to discover their physical locations (github.com/christianrowlands)
    20comments
  25. Nokia Design Archive (2025) (aalto.fi)
    121comments
  26. Forging 1024-bit RSA signatures in nearly SNFS time [pdf] (iacr.org)
    9comments
  27. Geothermal heat map of US hot springs (soakingsprings.com)
    39comments
  28. The Bayeux Tapestry: Woven by the Victors (historytoday.com)
    3comments
  29. Stable (YC W20) Is Hiring Product Engineers (usestable.com)
    —discuss
  30. Motor Characterization for Small Running Robots (2016) (robot-daycare.com)
    2comments

Discover and Prevent Linux Kernel Zero-Day Exploit Using Formal Verification

3 pointsby 5y agodigamma.ai
3 comments
5y agoHN ↗

[Coq, VST, CompCert]

Formal methods: https://en.wikipedia.org/wiki/Formal_methods

Formal specification: https://en.wikipedia.org/wiki/Formal_specification

Implementation of formal specification: https://en.wikipedia.org/wiki/Anti-pattern#Software_engineer...

Formal verification: https://en.wikipedia.org/wiki/Formal_verification

From "Why Don't People Use Formal Methods?" https://news.ycombinator.com/item?id=18965964 :

Which universities teach formal methods?

- q=formal+verification https://www.class-central.com/search?q=formal+verification

- q=formal+methods https://www.class-central.com/search?q=formal+methods

Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?

5y agoHN ↗

Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?

5y agoHN ↗

Formal methods could be used to prevent side channel attacks. However preventing each type of attack requires specifying properties which needs to be proven to assure it is is not possible. I am not very famililiar with TLA+, but I think in general it is not guaranteed to provide side channel attacks, such as based on timing, CPU state, etc.