🇺🇦 non-standard nerd on Nostr: Is there any open source tool for proving assertions about machine code programs, ...
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.
Published at
2024-12-19 05:26:35Event JSON
{
"id": "c58a96b99749f433ada0fbb9a16b1573050517bd9ac021d77056235b87225dba",
"pubkey": "9fc7078b50a6a7ba10f9f466689d342e63e26e30961c519d8abff37cac3a480c",
"created_at": 1734585995,
"kind": 1,
"tags": [
[
"proxy",
"https://mastodon.social/users/brouhaha/statuses/113677827788738854",
"activitypub"
]
],
"content": "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\".\n\nOpen source needed because I'd want to adapt the tool for a proprietary and very unconventional processor architecture.",
"sig": "6b041947d87aa027f83c352a2b7c469139bd214990a93a515e89661ed6031dc1f4c29d3de062b3149fcfeb6c6b852a805951f6ef669babdecc55649ce2f53753"
}
