Conversation

Notices

1. Embed this notice
   🇺🇦 haxadecimal (brouhaha@mastodon.social)'s status on Friday, 20-Dec-2024 17:21:57 JST 🇺🇦 haxadecimal

   Is there any open source tool for proving assertions about machine code programs, given some minimal constraints (e.g., no self-modifyimg code, all computed branch targets identified)? Assertions like "the carry flag will always be clear when this instruction starts execution".

   Open source needed because I'd want to adapt the tool for a proprietary and very unconventional processor architecture.

   • alcinnz repeated this.
   • Embed this notice
     Hovav Shacham (hovav@infosec.exchange)'s status on Friday, 20-Dec-2024 17:22:02 JST Hovav Shacham

     in reply to

     @brouhaha Vale, perhaps? https://github.com/project-everest/vale