sergey bratus

Twelfth LangSec IEEE Security & Privacy workshop is pleased to publish its preliminary schedule: langsec.org/spw26/program.… Join us on May 21 in San Francisco!

The internet has survived a period where a handful of late teens and early 20s kids were the only ones that knew about pre-malloc integer overflows as a bug class, and you could "grep malloc | grep \*" to find a bug in OpenSSH. This is why I am pretty chill about Mythos.

We are thrilled to announce that the workshop on Software Understanding and Reverse Engineering (SURE) is back for its second iteration, co-located with ACM CCS in The Hague! We invite the community to submit their research to SURE: sure-workshop.org/cfp/

Twelfth LangSec IEEE Security & Privacy workshop announces the panelist line-up for the Panel on LangSec and AI for formal methods: #panel" target="_blank" rel="nofollow noopener">langsec.org/spw26/agenda.h… Join us on May 21 is San Francisco!

LangSec has long been a forum for discussing the industry’s next hard problems. I’m excited to contribute to the panel on LangSec and AI for Formal Methods. AI is changing how software is built, deployed, and trusted, and reshaping how we think about trust itself.

Twelfth LangSec IEEE Security & Privacy workshop announces its preliminary agenda langsec.org/spw26/abstract… . Join us on May 21 for two keynotes on formal methods reaching broad industry practice, a panel on AI & LangSec, and talks. Work-in-progress reports and more TBA soon.

One of my favorite newer, and lesser known paper from Tony Hoare: Concurrent Kleene Algebra — opus.bibliothek.uni-augsburg.de/opus4/frontdoo… — this paper inspired me to study the algebraic approach to program and network verification. (KATs, NetKATs, algebras of incorrectness, etc.)

POV: You are a security researcher looking to advance the state of the art and science in offensive security. Submit to WOOT and show us all the hacks you're cooking up 🧑‍🍳

A curious example of misaligned defense: a recipe site aggressively profiles browsers, likely to avoid LLM crawlers. Frustrated users give up and go to ask an LLM for the recipe. So it goes.

Velvet, our automated Dafny-style verifier embedded into Lean, has moved to a new repository as a standalone Lean library: github.com/verse-lab/velv… Give it a try!

I must be getting old because I see people taking about “skills” and how they can be malicious and how some people are building “skill scanners” and I have a hard time understanding how we messed up so bad we made text files dangerous

The damage done by fictional descriptions of cyber attack, in taking up decisionmakers mindshare without real substance, is an incalculable cost to the employment of instruments of national power. Even moreso where these fictions are spun by those purporting to some journalist proximity. All of which downplays real effects and the hard necessary business of campaigning.

A reminder that the Twelfth Language-theoretic IEEE Security & Privacy workshop's call for papers is open through Feb 13, langsec.org/spw26/ Please submit your work and join us at IEEE S&P Workshops day, May 21, 2026, in San Francisco!

One thing my team learned in the past two years of building pragmatic program verifiers is that their performance matters at least as much if not more than expressivity, both for humans and AI automation. As most of programs/specs are broken initially, fast turnaround is a must.

@HostileSpectrum Some papers are long overdue :)

@sergeybratus If you put that evil on me, one is certain you might be cursed to be the peer review. And one expects it would be painful in comparison to your usual standard.

What is the tipping point to novel failure modes when a sufficient percentage of the bureaucracy is nothing more than mid level paper pushers with no substantive experiences of their own, trading AI generated slop back and forth ad infinitium, each desperately hoping to avoid being caught anywhere near a real decision that might have consequences?

The quality of reasoning/logic progressed so quickly over the last year that things are becoming possible in many directions I was previously quite skeptical about. The only thing that matters now is context (domain-specific expertise) and the velocity of access to knowledge of new attack classes. Exploit development has always been manual, human-centric work because it requires specific expertise not frequently accessible to the public. Now, AI can figure it out independently based on existing knowledge.

Really hoping to see formal verification act as the security guardrails for AI-generated code this year.

@matrosov A panel on combining AI and formal methods for a breakthrough much greater than the sum of the parts would be very timely! Now would be a great time to submit a proposal for one :)

The LangSec'26 IEEE Security & Privacy workshop call for papers will remain open until February 13. Please submit your work & join us on May 21, 2026 in San Francisco! langsec.org/spw26/