Hacker News

Top stories

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

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

3 pointsby 5y agodigamma.ai
Open original View on HN
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.

Open thread on HN ↗