About SAT@home:

SAT@home is a research project that uses Internet-connected computers to solve hard and practically important problems (discrete functions inversion problems, discrete optimization, bioinformatics, etc) that can be effectively reduced to SAT. Currently in the project problems of inversion of some cryptographic functions used in keystream generators are being solved. All cryptographic algorithms under investigation are publicly available. Corresponding tasks are randomly generated and do not contain any confidential information. We also plan to publish obtained results. In the nearest future we are going to launch an experiment for solving Quadratic Assignment problem (as a SAT problem) within the project. Project was implemented using DC-API.


SAT@home is suppoted by:

Institute for Systems Analysis of Russian Academy of Sciences, department of Distributed Computing - a founding member of the International Desktop Grid Federation
Institue for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Science, laboratory of Discrete Analysis and Applied Logic.


Scientific goal of the project

The project is aimed to solve various combinatorial problems. There are many practically important problems for which the existence of effective (polynomial) algorithms of their solving has not been proven. Most of these problems are NP-hard. It means that under some reasonable (albeit unproven) assumptions, these problems can not be solved in polynomial time. However, many of their special cases arise in practical applications: various discrete optimization problems (for example, planning of production) and problems of verification of discrete devices (arising, for example, in designing of circuits and proving of program correctness). Therefore it is very important to have methods for their solving that don't have polynomial complexity, but are effective in practice. Such methods can cope with the numerous special cases of NP-hard problems of huge dimensions. One of the most simple in its basis, and therefore the most efficient in terms of software implementations is SAT approach. This approach is based on reducibility of the considered original problem to a SAT problem, that is the problem of satisfiability of conjunctive normal form (CNF). SAT problems admit a very natural form of parallelism, allowing use of a distributed computing environments (including Grid). Actually reducibility to SAT can be carried out effectively (in fact, it follows from the famous theorem of Cook-Levin).

Cryptanalysis provides very attractive class of problems for solving of which SAT approach can be used. It should be noted that we don't solve problems of deciphering some private data. All the tests under consideration are randomly generated. In this regard, our work is to study stability of modern encryption systems. Our strongest practical result is successful logical cryptanalysis (i.e. in the form of SAT problem) of the keystream generator that is used in well-known cipher A5/1. This result was obtained in 2009 with the use of BNB-Grid (paper in journal of ISA RAS, paper on Arxiv, paper in Lecture Notes in Computer Science). In 2010-2011, there were investigations (see, for example, this source), in which real cryptanalysis of A5/1 was also carried out, but using different methods. In fact, an advanced technique of rainbow tables was used. But even the best rainbow tables do not cover all the key space to 100%. Therefore, in the nearest future, we plan to solve in the project SAT@home problems of search for initialization sequences for A5/1 that are not covered by the best known rainbow tables.

Further we plan to use SAT@home to study other cryptographic functions and solve some 'extremely hard' problems of discrete optimization, in particular the Quadratic Assignment Problem (QAP), and some bioinformatics problems (analysis of discrete models of gene networks).






Sobre SAT@home:

Sat@home es un proyecto de investigación que utiliza ordenadores conectados a Internet para resolver problemas difíciles e importantes en la práctica (problemas discretos inversión de funciones, optimización discreta, bioinformática, etc) que pueden ser reducidas a SAT. Actualmente en los problemas del proyecto de inversión de algunas funciones criptográficas utilizadas en los generadores de flujo de clave se están resolviendo. Todos los algoritmos de cifrado en la investigación están disponibles al público. Las tareas correspondientes son generadas al azar y no contienen ninguna información confidencial. También tenemos previsto publicar los resultados obtenidos. En un futuro próximo vamos a lanzar un experimento para la solución de problemas de asignación cuadrática (como un problema SAT) dentro del proyecto. Proyecto se ha realizado utilizando DC-API.


SAT@home está respaldado por:

Instituto para el Análisis de Sistemas de la Academia Rusa de Ciencias, Departamento de Computación Distribuida - miembro fundador de la International Desktop Grid Federación
Instituto para la Dinámica de Sistemas y Teoría de Control de la rama siberiana de la Academia Rusa de Ciencias, Laboratorio de Análisis Discreto y Lógica Aplicada.


Objetivo científico del proyecto

El proyecto está dirigido a resolver diversos problemas combinatorios. Hay muchos problemas importantes para las que prácticamente la existencia de eficaces (polinomio) algoritmos de su resolución de no ha sido comprobado. La mayoría de estos problemas son NP-hard. Esto significa que bajo ciertas razonables (aunque no demostrada) de supuestos, estos problemas no pueden ser resueltos en tiempo polinómico. Sin embargo, muchos de sus casos especiales surgen en las aplicaciones prácticas: varios problemas de optimización discretos (por ejemplo, la planificación de la producción) y los problemas de verificación de dispositivos discretos (procedentes, por ejemplo, en el diseño de circuitos y comprobar la corrección del programa). Por lo tanto, es muy importante disponer de métodos para su resolución de que no tienen complejidad polinómica, pero son eficaces en la práctica. Tales métodos pueden hacer frente a los numerosos casos especiales de NP-difíciles problemas de grandes dimensiones. Uno de los más simples en su base, y por lo tanto el más eficiente en términos de las implementaciones de software se sáb enfoque. Este enfoque se basa en la reducibilidad del problema considerado original a un problema SAT, que es el problema de satisfactibilidad de forma normal conjuntiva (CNF). Problemas sáb admitir una forma muy natural de paralelismo, permitiendo el uso de un entorno de computación distribuida (incluyendo Grid). En realidad reducibilidad a SAT se puede llevar a cabo con eficacia (de hecho, se desprende del famoso teorema de Cook-Levin).

El Criptoanálisis ofrece clase muy atractiva de problemas para resolver de los cuales sáb enfoque puede ser utilizado. Cabe señalar que no se resuelven los problemas de descifrar algunos datos privados. Todas las pruebas que se examinan son generados aleatoriamente. En este sentido, nuestro trabajo es estudiar la estabilidad de los sistemas de cifrado modernos. Nuestro fuerte resultado práctico es criptoanálisis exitoso lógico (es decir, en forma de problema SAT) del generador de flujo de clave que se utiliza en el conocido sistema de cifrado A5 / 1. Este resultado se obtuvo en 2009 con el uso de BNB-Grid (artículo en la revista de ISA RAS, en Arxiv papel, papel en Lecture Notes in Computer Science). En 2010-2011, hubo investigaciones (véase, por ejemplo, esta fuente), en el que el criptoanálisis real de A5 / 1 también se llevó a cabo, pero usando diferentes métodos. De hecho, una técnica avanzada de tablas de arco iris se utilizó. Pero incluso las mejores tablas de arco iris no cubren todo el espacio clave para el 100%. Por lo tanto, en el futuro próximo, tenemos previsto resolver en el proyecto sáb @ home problemas de búsqueda de secuencias de inicialización para A5 / 1 que no están cubiertos por las mejores mesas del arco iris conocidos.

Además tenemos la intención de utilizar sat@home para estudiar otras funciones criptográficas y resolver algunos "extremadamente duras" problemas de optimización discreta, en particular el problema de asignación cuadrática (QAP), y algunos problemas de la bioinformática (análisis de modelos discretos de las redes de genes).







http://sat.isa.ru/pdsat/apps.php








Url del proyecto: http://sat.isa.ru/pdsat/index.php

Url del equipo: http://sat.isa.ru/pdsat/team_display.php?teamid=31

Server Status: http://sat.isa.ru/pdsat/server_status.php