På EE Times dök det upp en artikel om en ny algoritm som kan mycket snabbt kan hitta symmetrier. Algoritmen i fråga heter Saucy och artikeln beskriver Saucy:
Combinatorial problems are one of the toughest nuts to crack in design automation and other applications that sift data. For instance, the number of Internet router path combinations for sending a message around the world is enormous. The shortest path is seldom chosen because there is no way to find the optimal distance among so many possibilities.Now, the developers of an algorithm called “Saucy” claim it can solve such problems quickly by finding symmetries among large swaths of possibilities. In the global Internet routing problem, Saucy found so many symmetries—10 with 83,687 zeros—that it could sort through and an find an optimum path in under a second. Saucy was described this week at the Design Automation Conference.
Att artikeln presenterades på DAC-konferensen är inte så konstigt. Symmetriproblem finns det en stor mängd av inom EDA-området. Formell verifiering genom ekvivalenscheck är ett exempel där grafisomorfism används för att jämföra två konstruktioner.
Ett exempel – följande två grafer är isomorfa:
Andra EDA-områden där det finns symmetriproblem är syntes (BDD-träd), routing och layout. Eftersom Moores lag stampar vidare med fortsatt snabbt växande konstruktioner behöver verktygen bli allt snabbare för att inte utvecklingstiden skall skena iväg.
Saucy är utvecklad op University of Michigan och Berkeley. På sidan för Saucy-projektet finns mer information, bland annat ett par artiklar och en relativt ny presentation. På sidan sammanfattas Saucy med:
Many computational tools have recently begun to benefit from the use of the symmetry inherent in the tasks they solve, and use general-purpose graph symmetry tools to uncover this symmetry. However, existing tools suffer quadratic runtime in the number of symmetries explicitly returned and are of limited use on very large, sparse, symmetric graphs.This paper introduces a new symmetry-discovery algorithm which exploits the sparsity present not only in the input but also the output, i.e., the symmetries themselves. By avoiding quadratic runtime on large graphs, it improves state-of-the-art runtimes from several days to less than a second.
Detta låter kanonbra, och är man som jag intresserad av EDA-verktyg och elektronikdesign är detta mycket spännande. Men varför ta upp detta på Kryptoblog?
Jo på grund av symmetriproblem och snabba lösningar av SAT-problem, vilket är samma slags problem som BDD-träd och isomorfism, går att använda för kryptanalys.
Några exempel på detta hittar vi i artiklarna Applications of SAT Solvers to Cryptanalysis of Hash Functions (pdf) och Logical Cryptanalysis as a SAT Problem: the Encoding of the Data Encryption Standard.
Den första artikeln (av Ilya Mironov och Lintao Zhang från Microsoft) är relativt ny och sammanfattningen av artikeln beskriver användningen av algoritmer för SAT-problem:
Several standard cryptographic hash functions were broken in 2005. Some essential building blocks of these attacks lend themselves well to automation by encoding them as CNF formulas, which are within reach of modern SAT solvers.In this paper we demonstrate effectiveness of this approach. In particular, we are able to generate full collisions for MD4 and MD5 given only the differential path and applying a (minimally modified) off-the-shelf SAT solver.
To the best of our knowledge, this is the first example of a SAT-solver-aided cryptanalysis of a non-trivial cryptographic primitive. We expect SAT solvers to find new applications as a validation and testing tool of practicing cryptanalysts.
Det skulle vara otroligt intressant att se om det går att applicera Saucy på den attack mot hashfunktioner som Ilya Mironov och Lintao Zhang beskriver. Någon som är intresserad av att sponsra ett forskningsprojekt? 😉
No related posts.
Related posts brought to you by Yet Another Related Posts Plugin.
