{"id":30551,"date":"2026-05-07T10:27:32","date_gmt":"2026-05-07T08:27:32","guid":{"rendered":"https:\/\/tinextadefence.it\/?p=30551"},"modified":"2026-05-07T10:27:32","modified_gmt":"2026-05-07T08:27:32","slug":"escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers","status":"publish","type":"post","link":"https:\/\/tinextadefence.it\/en\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/","title":{"rendered":"Escaping the Maze \u2013 A Z3 Solver Tutorial for Reverse Engineers"},"content":{"rendered":"

In the context of malware analysis, the\u00a0<\/span>Reverse engineering<\/span><\/i>\u00a0Custom ciphers present a challenge: when an algorithm combines multiple layers of permutation, key mixing, and substitution, manual analysis slows down and quickly becomes more complex and inaccurate.<\/span><\/p>\n

The new study from\u00a0<\/span>Malware Lab<\/span><\/b>\u00a0show how to overcome this limitation by using\u00a0<\/span>Z3<\/span><\/b>, an SMT solver developed by Microsoft Research that, instead of manually inverting the cipher, models the function in symbolic form, leaving the solver to automatically reconstruct its inverse.<\/span><\/p>\n

Based on a real case, starting from a\u00a0<\/span>Substitution-Permutation Network from KALMAR CTF 2024<\/span><\/b>, this analysis shows how Z3's methodology is directly applicable also to the analysis of\u00a0<\/span>loader, ransomware e packer<\/span>.<\/span><\/p>\n

After introducing the operating principles of Z3, the study illustrates a complete solving script, delves into the topic of symbolic indexes and concludes with an account of the main difficulties encountered in its initial applications.<\/span>\u00a0<\/span><\/p>\n

If you wish to learn more, here is the link to our\u00a0<\/span>comprehensive study<\/span><\/b><\/a>.<\/span><\/p>\n

In addition, you can subscribe to the specific mailing list\u00a0<\/span>Cyber Studios by T-Defence<\/span><\/b>, to receive updates on upcoming research:<\/span><\/p>\n

https:\/\/tinextadefence.it\/mailing-list-cyber-studios\/<\/span><\/a><\/p>","protected":false},"excerpt":{"rendered":"

Nel contesto della malware\u00a0analysis,\u00a0il\u00a0reverse\u00a0engineering\u00a0di cifrari personalizzati rappresenta una sfida: quando un algoritmo combina pi\u00f9 livelli di permutazione, mescolamento delle chiavi e sostituzione, l\u2019analisi manuale\u00a0rallenta e\u00a0diventa rapidamente\u00a0pi\u00f9\u00a0complessa\u00a0e imprecisa. Il nuovo studio del\u00a0Malware Lab\u00a0mostra come superare questo limite\u00a0utilizzando\u00a0Z3, un solver SMT sviluppato da Microsoft\u00a0Research\u00a0che\u00a0invece di\u00a0invertire manualmente il cifrario,\u00a0modella la\u00a0funzione\u00a0in\u00a0forma simbolica, lasciando al solver il compito di ricostruirne […]<\/p>","protected":false},"author":7,"featured_media":30552,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[102],"tags":[],"class_list":["post-30551","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-tinextadefencebusiness"],"acf":[],"yoast_head":"\nEscaping the Maze - A Z3 Solver Tutorial for Reverse Engineers - Tinexta Defence<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/tinextadefence.it\/en\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/\" \/>\n<meta property=\"og:locale\" content=\"en_GB\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Escaping the Maze - A Z3 Solver Tutorial for Reverse Engineers - Tinexta Defence\" \/>\n<meta property=\"og:description\" content=\"Nel contesto della malware\u00a0analysis,\u00a0il\u00a0reverse\u00a0engineering\u00a0di cifrari personalizzati rappresenta una sfida: quando un algoritmo combina pi\u00f9 livelli di permutazione, mescolamento delle chiavi e sostituzione, l\u2019analisi manuale\u00a0rallenta e\u00a0diventa rapidamente\u00a0pi\u00f9\u00a0complessa\u00a0e imprecisa. Il nuovo studio del\u00a0Malware Lab\u00a0mostra come superare questo limite\u00a0utilizzando\u00a0Z3, un solver SMT sviluppato da Microsoft\u00a0Research\u00a0che\u00a0invece di\u00a0invertire manualmente il cifrario,\u00a0modella la\u00a0funzione\u00a0in\u00a0forma simbolica, lasciando al solver il compito di ricostruirne […]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/tinextadefence.it\/en\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/\" \/>\n<meta property=\"og:site_name\" content=\"Tinexta Defence\" \/>\n<meta property=\"article:published_time\" content=\"2026-05-07T08:27:32+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"1800\" \/>\n\t<meta property=\"og:image:height\" content=\"960\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"author\" content=\"Federica Casadei\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"Federica Casadei\" \/>\n\t<meta name=\"twitter:label2\" content=\"Estimated reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"2 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#article\",\"isPartOf\":{\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/\"},\"author\":{\"name\":\"Federica Casadei\",\"@id\":\"https:\/\/tinextadefence.it\/#\/schema\/person\/0dc89f3eeaa8cd7b7c354b61c84d164d\"},\"headline\":\"Escaping the Maze – A Z3 Solver Tutorial for Reverse Engineers\",\"datePublished\":\"2026-05-07T08:27:32+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/\"},\"wordCount\":191,\"commentCount\":0,\"publisher\":{\"@id\":\"https:\/\/tinextadefence.it\/#organization\"},\"image\":{\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg\",\"articleSection\":[\"#TDefenceBusiness\"],\"inLanguage\":\"en-GB\",\"potentialAction\":[{\"@type\":\"CommentAction\",\"name\":\"Comment\",\"target\":[\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#respond\"]}]},{\"@type\":\"WebPage\",\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/\",\"url\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/\",\"name\":\"Escaping the Maze - A Z3 Solver Tutorial for Reverse Engineers - Tinexta Defence\",\"isPartOf\":{\"@id\":\"https:\/\/tinextadefence.it\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#primaryimage\"},\"image\":{\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg\",\"datePublished\":\"2026-05-07T08:27:32+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#breadcrumb\"},\"inLanguage\":\"en-GB\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-GB\",\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#primaryimage\",\"url\":\"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg\",\"contentUrl\":\"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg\",\"width\":1800,\"height\":960},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/tinextadefence.it\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Escaping the Maze – A Z3 Solver Tutorial for Reverse Engineers\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/tinextadefence.it\/#website\",\"url\":\"https:\/\/tinextadefence.it\/\",\"name\":\"Tinexta Defence\",\"description\":\"think next, protect now\",\"publisher\":{\"@id\":\"https:\/\/tinextadefence.it\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/tinextadefence.it\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-GB\"},{\"@type\":\"Organization\",\"@id\":\"https:\/\/tinextadefence.it\/#organization\",\"name\":\"Tinexta Defence\",\"url\":\"https:\/\/tinextadefence.it\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-GB\",\"@id\":\"https:\/\/tinextadefence.it\/#\/schema\/logo\/image\/\",\"url\":\"https:\/\/tinextadefence.it\/wp-content\/uploads\/2025\/03\/Tinexta_Defence_marchio.png\",\"contentUrl\":\"https:\/\/tinextadefence.it\/wp-content\/uploads\/2025\/03\/Tinexta_Defence_marchio.png\",\"width\":2000,\"height\":990,\"caption\":\"Tinexta Defence\"},\"image\":{\"@id\":\"https:\/\/tinextadefence.it\/#\/schema\/logo\/image\/\"}},{\"@type\":\"Person\",\"@id\":\"https:\/\/tinextadefence.it\/#\/schema\/person\/0dc89f3eeaa8cd7b7c354b61c84d164d\",\"name\":\"Federica Casadei\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-GB\",\"@id\":\"https:\/\/tinextadefence.it\/#\/schema\/person\/image\/\",\"url\":\"https:\/\/secure.gravatar.com\/avatar\/6b35becb35fb83a681c7b431c36de302b4101b5ef0c48984910308c04617428f?s=96&d=mm&r=g\",\"contentUrl\":\"https:\/\/secure.gravatar.com\/avatar\/6b35becb35fb83a681c7b431c36de302b4101b5ef0c48984910308c04617428f?s=96&d=mm&r=g\",\"caption\":\"Federica Casadei\"}}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Escaping the Maze - A Z3 Solver Tutorial for Reverse Engineers - Tinexta Defence","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/tinextadefence.it\/en\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/","og_locale":"en_GB","og_type":"article","og_title":"Escaping the Maze - A Z3 Solver Tutorial for Reverse Engineers - Tinexta Defence","og_description":"Nel contesto della malware\u00a0analysis,\u00a0il\u00a0reverse\u00a0engineering\u00a0di cifrari personalizzati rappresenta una sfida: quando un algoritmo combina pi\u00f9 livelli di permutazione, mescolamento delle chiavi e sostituzione, l\u2019analisi manuale\u00a0rallenta e\u00a0diventa rapidamente\u00a0pi\u00f9\u00a0complessa\u00a0e imprecisa. Il nuovo studio del\u00a0Malware Lab\u00a0mostra come superare questo limite\u00a0utilizzando\u00a0Z3, un solver SMT sviluppato da Microsoft\u00a0Research\u00a0che\u00a0invece di\u00a0invertire manualmente il cifrario,\u00a0modella la\u00a0funzione\u00a0in\u00a0forma simbolica, lasciando al solver il compito di ricostruirne […]","og_url":"https:\/\/tinextadefence.it\/en\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/","og_site_name":"Tinexta Defence","article_published_time":"2026-05-07T08:27:32+00:00","og_image":[{"width":1800,"height":960,"url":"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg","type":"image\/jpeg"}],"author":"Federica Casadei","twitter_card":"summary_large_image","twitter_misc":{"Written by":"Federica Casadei","Estimated reading time":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#article","isPartOf":{"@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/"},"author":{"name":"Federica Casadei","@id":"https:\/\/tinextadefence.it\/#\/schema\/person\/0dc89f3eeaa8cd7b7c354b61c84d164d"},"headline":"Escaping the Maze – A Z3 Solver Tutorial for Reverse Engineers","datePublished":"2026-05-07T08:27:32+00:00","mainEntityOfPage":{"@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/"},"wordCount":191,"commentCount":0,"publisher":{"@id":"https:\/\/tinextadefence.it\/#organization"},"image":{"@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#primaryimage"},"thumbnailUrl":"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg","articleSection":["#TDefenceBusiness"],"inLanguage":"en-GB","potentialAction":[{"@type":"CommentAction","name":"Comment","target":["https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#respond"]}]},{"@type":"WebPage","@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/","url":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/","name":"Escaping the Maze - A Z3 Solver Tutorial for Reverse Engineers - Tinexta Defence","isPartOf":{"@id":"https:\/\/tinextadefence.it\/#website"},"primaryImageOfPage":{"@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#primaryimage"},"image":{"@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#primaryimage"},"thumbnailUrl":"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg","datePublished":"2026-05-07T08:27:32+00:00","breadcrumb":{"@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#breadcrumb"},"inLanguage":"en-GB","potentialAction":[{"@type":"ReadAction","target":["https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/"]}]},{"@type":"ImageObject","inLanguage":"en-GB","@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#primaryimage","url":"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg","contentUrl":"https:\/\/tinextadefence.it\/wp-content\/uploads\/2026\/05\/Business_evidenza.jpg","width":1800,"height":960},{"@type":"BreadcrumbList","@id":"https:\/\/tinextadefence.it\/escaping-the-maze-a-z3-solver-tutorial-for-reverse-engineers\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/tinextadefence.it\/"},{"@type":"ListItem","position":2,"name":"Escaping the Maze – A Z3 Solver Tutorial for Reverse Engineers"}]},{"@type":"WebSite","@id":"https:\/\/tinextadefence.it\/#website","url":"https:\/\/tinextadefence.it\/","name":"Tinexta Defence","description":"think next, protect now","publisher":{"@id":"https:\/\/tinextadefence.it\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/tinextadefence.it\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-GB"},{"@type":"Organization","@id":"https:\/\/tinextadefence.it\/#organization","name":"Tinexta Defence","url":"https:\/\/tinextadefence.it\/","logo":{"@type":"ImageObject","inLanguage":"en-GB","@id":"https:\/\/tinextadefence.it\/#\/schema\/logo\/image\/","url":"https:\/\/tinextadefence.it\/wp-content\/uploads\/2025\/03\/Tinexta_Defence_marchio.png","contentUrl":"https:\/\/tinextadefence.it\/wp-content\/uploads\/2025\/03\/Tinexta_Defence_marchio.png","width":2000,"height":990,"caption":"Tinexta Defence"},"image":{"@id":"https:\/\/tinextadefence.it\/#\/schema\/logo\/image\/"}},{"@type":"Person","@id":"https:\/\/tinextadefence.it\/#\/schema\/person\/0dc89f3eeaa8cd7b7c354b61c84d164d","name":"Federica Casadei","image":{"@type":"ImageObject","inLanguage":"en-GB","@id":"https:\/\/tinextadefence.it\/#\/schema\/person\/image\/","url":"https:\/\/secure.gravatar.com\/avatar\/6b35becb35fb83a681c7b431c36de302b4101b5ef0c48984910308c04617428f?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/6b35becb35fb83a681c7b431c36de302b4101b5ef0c48984910308c04617428f?s=96&d=mm&r=g","caption":"Federica Casadei"}}]}},"_links":{"self":[{"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/posts\/30551","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/users\/7"}],"replies":[{"embeddable":true,"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/comments?post=30551"}],"version-history":[{"count":0,"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/posts\/30551\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/media\/30552"}],"wp:attachment":[{"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/media?parent=30551"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/categories?post=30551"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/tinextadefence.it\/en\/wp-json\/wp\/v2\/tags?post=30551"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}