Raineraineyang.hashnode.dev·Aug 9, 2024PyTA Project: Augment CFG Edges with Z3 ConstraintsToday's task requires a combination of various components of PythonTA introduced in previous articles, including control flow graph module, Z3 visitor, and Z3 expression wrapper. In this task, we will augment each control flow graph edge with a list ...Python
Raineraineyang.hashnode.dev·Jul 18, 2024PyTA Project: Converting String Expressions to Z3 ConstraintsThis article is a continuation of the previous task , which implements the parsing of container types (list/set/tuple) and operators to Z3 constraints. In today's task, we will implement the parsing for string variables and corresponding operators, i...Python
Raineraineyang.hashnode.dev·Jul 3, 2024PyTA Project: Converting Function Preconditions to Z3 ConstraintsToday's task is to update ExprWrapper, a module that converts a python expression to corresponding z3 expression, to support container classes like list , tuple, and set, and in operation. In this article, I will first provide a brief overview of z3 ...Python
Tomasz Węgrzanowskitaw.hashnode.dev·Jan 1, 2023Break XOR Cipher with Z3In previous post, I showed how to break Caesar cipher with Z3. This wasn't really all that exciting as Caesar cipher has only 26 possibilities, so it's triival to break with brute force, and you can even just display all possible answers and choose t...52 readsz3
Tomasz Węgrzanowskitaw.hashnode.dev·Dec 31, 2022Break Caesar Cipher with Z3Z3 is usually given a list of hard constraints, and told to solve them, but it can do quite a few more things. Let's use it unconventionally and break Caesar cipher. The Challenge The following plaintext from Wikipedia: In cryptography, a Caesar cip...Ruby
Kamil Gierach-Pacanekblog.cyberethical.me·Nov 23, 2022Solving Equations Like A ProBackground On October I have participated in MSHP CTF and one of the challenges intrigued me so much that I promised myself to create a separate article on that. Challenge Following screen is my recreation of the challenge. Original application made...1.4K readsz3
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 16, 2022Open Source Adventures: Episode 74: Crystal Z3 Solver for Light Up PuzzleThis is the final episode with Crystal Z3 solvers, at least for now. In previous episode I showed how to solve Lights Up puzzle with math, now it's time to write a Crystal Z3 solver. Light Up (Akari) is a simple puzzle with following rules: there's ...Open Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 15, 2022Open Source Adventures: Episode 73: How to solve Light Up Puzzle with mathLight Up (Akari) is a simple puzzle with following rules: there's a grid of cells some cells are wall cells your task is to place light bulbs in some of the cells light spreads horizontally and vertically from light bulbs, but it doesn't pass throug...Open Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 10, 2022Open Source Adventures: Episode 72: Crystal Z3 Solver for Dominosa PuzzleDominosa is a puzzle with simple rules: there's a grid filled with numbers you need to pair those numbers into dominos each domino needs to be different As usual, I recommend playing the puzzle a few times to get a good feel for it. It will make it...Open Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 9, 2022Open Source Adventures: Episode 71: Improving Crystal Z3 ShardWhile writing various puzzle game solvers in Crystal Z3 I discovered two big issues: I frequently needed .reduce chains of +/*/and/or with special case for empty arrays Model#[] returned untyped result (Expr) even though its exact type is statically...Open Source Adventurescrystal
