Hacker News

Top stories

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

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.