search

sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.41k stars 475 forks source link

Fix var() method for cryptominisat and picosat, which breaks solve_sat for boolean polynomial systems #26676

Closed hadipourh closed 5 years ago

hadipourh commented 5 years ago

When I used Sage7.2, I could easily solve my boolean equations with solve_sat commands, and it's results were verified by the papers and other tools, but when I upgraded my sage to version 8 (or later version) I found that the new solve_sat solver (especially when we use CryptoMiniSat as the SAT solver) doesn't work as correct as before. For example, when I solve a system of equations via solve_sat which used CryptoMiniSat as a SAT solver, I get different number of solutions in different version of SageMath. I believe that there is something wrong in newer version of SageMath because my previous experiences shows that the older version's results were verified by the other tools and papers. I hope someone could solve this problem.

See also the following thread on sage-devel: https://groups.google.com/forum/?fromgroups#!topic/sage-devel/2EhgHzGgUnQ

CC: @sagetrac-tmonteil

Component: packages: optional

Keywords: solve_sat, CryptoMiniSat, picosat

Author: Thierry Monteil

Branch/Commit: c492724

Reviewer: Frédéric Chapoton

Issue created by migration from https://trac.sagemath.org/ticket/26676

jdemeyer commented 5 years ago
comment:1

Can you be more concrete exactly what the problem is?

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago
comment:2

As suggested by Jeroen, you should provide explicit (if possible minimal) code so that we can understand the actual issue and work from something. There might indeed be an issue with boolean equations since it relied on a learnt_clauses method that does not exist anymore, and the code lacks of doctests.

By the way, a good way to hint some developer about an issue is to add her nickname in the CC field so that she could recieve an email. In the title, author field or keywords field, only the people who have a regular look at the timeline will notice.

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago

Changed author from Thierry Monteil to none

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago

Changed keywords from solve_sat, Thierry Monteil, CryptoMiniSat to solve_sat, CryptoMiniSat

hadipourh commented 5 years ago
comment:3

Replying to @sagetrac-tmonteil:

As suggested by Jeroen, you should provide explicit (if possible minimal) code so that we can understand the actual issue and work from something. There might indeed be an issue with boolean equations since it relied on a learnt_clauses method that does not exist anymore, and the code lacks of doctests.

By the way, a good way to hint some developer about an issue is to add her nickname in the CC field so that she could recieve an email. In the title, author field or keywords field, only the people who have a regular look at the timeline will notice.

Dear Monteli,

Regarding to explicit code for understanding the actual issue: I'll upload a code that generate a system of boolean equations which shows the issue exactly. This system of equations is extracted from a stream cipher called Bivium-B and I've solved it several times in Sage 7.2, and I'm certain that it has a unique solution, but when I want to solve it via the newer versions of SageMath (after 8.0), solver returns False as the output, which means there is not any solutions! I'll upload the code as soon as possible.

Thanks in advance for your help

8d2daa01-d1db-4916-95ec-d66a71da2bf4 commented 5 years ago

Attachment: ph1234.pdf.gz

hadipourh commented 5 years ago
comment:4

Replying to @hadipourh:

Replying to @sagetrac-tmonteil:

As suggested by Jeroen, you should provide explicit (if possible minimal) code so that we can understand the actual issue and work from something. There might indeed be an issue with boolean equations since it relied on a learnt_clauses method that does not exist anymore, and the code lacks of doctests.

By the way, a good way to hint some developer about an issue is to add her nickname in the CC field so that she could recieve an email. In the title, author field or keywords field, only the people who have a regular look at the timeline will notice.

Dear Monteli,

Regarding to explicit code for understanding the actual issue: I'll upload a code that generate a system of boolean equations which shows the issue exactly. This system of equations is extracted from a stream cipher called Bivium-B and I've solved it several times in Sage 7.2, and I'm certain that it has a unique solution, but when I want to solve it via the newer versions of SageMath (after 8.0), solver returns False as the output, which means there is not any solutions! I'll upload the code as soon as possible.

Thanks in advance for your help

Dear Monteli,

Here's the code which shows the issue. This script generates 441 cubic equations for the SBox of the AES cipher. The SBox is a bijective function from GF(2)8 to GF(2)8. for example let (y0, y1, ..., y7) = S(x0, x1, ..., x7) and we have system of 441 equations like this:

f1(x0, ..., x8, y0, ..., y7) = 0

.

.

.

f441(x0, ..., x8, y0, ..., y7) = 0

which it's solutions must satisfy the (y0, y1, ..., y7) = S(x0, x1, ..., x7) relation. Since S is a bijective function from GF(2)8 to GF(2)8, there are at least 256 solutions for the above system of equations. But when I used solve_sat to solve the above system of equations, it returned only 27 solutions which shows that the solve_sat can't find all solutions even the parameter "n" in solve_sat command is equal to "infinity"!

A Sage script which generates the cubic equations of the AES SBox and solves it via the solve_sat command:

from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence
from sage.sat.boolean_polynomials import solve as solve_sat
sr = sage.crypto.mq.SR(1, 4, 4, 8, allow_zero_inversions = True)
sb = sr.sbox()
eqs = sb.polynomials(degree = 3)
eqs = PolynomialSequence(eqs)
variables = map(str, eqs.variables())
variables = ",".join(variables)
R = BooleanPolynomialRing(16, variables)
eqs = map(R, eqs)
%time sls_aes = solve_sat(eqs, n = infinity, s_verbosity = 8)
print("Number of solutions = %s" % len(sls_aes))

When I executed the above code in my own laptop, I got the bellow solutions:

CPU times: user 6.49 s, sys: 10.3 s, total: 16.8 s
Wall time: 23.1 s
Number of solutions = 27

In addition, I feel the run-time of solve_sat has been increased in comparison with previous versions.

jvpeetz commented 5 years ago
comment:6

Hi,

I can add a small example which might help to fix the problem:

varl = ['k{0}'.format(p) for p in range(29)]  # no solution

B = BooleanPolynomialRing(names = varl)
B.inject_variables(verbose=False)

keqs = [
    k0 + k6 + 1,
    k3 + k9 + 1,
    k5*k18 + k6*k18 + k7*k16 + k7*k10,
    k9*k17 + k8*k24 + k11*k17,
    k1*k13 + k1*k15 + k2*k12 + k3*k15 + k4*k14,
    k5*k18 + k6*k16 + k7*k18,
    k3 + k26,
    k0 + k19,
    k9 + k28,
    k11 + k20]

from sage.sat.boolean_polynomials import solve as solve_sat

kpsol = solve_sat(keqs, n=1)

The Boolean equation system (ANF) definitly has a solution but solve_sat() returns False.

The interface to cryptominisat implemented in src/sage/sat/solvers/cryptominisat.py has a bug in the enumeration of the CNF variables. This bug results in faulty ANF to CNF conversion and failures in the solver routine sat.boolean_polynomials.solve().

When using the ANF to CNF converter CNFEncoder with the solver CryptoMiniSat (which the function sat.boolean_polynomials.solve() does) with this example some of the variable indices are re-used for different monomials of the ANF which is a bug.

The variable indices used when converting the fifth equation (k1*k13 + k1*k15 + k2*k12 + k3*k15 + k4*k14) get re-used when converting equations with the monomials k26 and k28.

When using the DIMACS solver instead, the conversion to CNF works correctly, the resulting CNF file can be solved by a SAT solver.

Comparing the functions in src/sage/sat/solvers/cryptominisat.py and src/sage/sat/solvers/dimacs.py I see discrepancies, for example in the functions var() and add_clause().

This bug is also present in the picosat binding, I think.

Any ideas?

Regards, Jörg.

jvpeetz commented 5 years ago
comment:7

A remedy for this bug is (at least for my little example) to change the var() function in local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.py (source file is in src/sage/sat/solvers/cryptominisat.py) from

        return self._nvars + 1

to

        self._nvars += 1
        return self._nvars

which corresponds to the code of the DIMACS solver. Removing the file cryptominisat.pyc, starting sage and importing CryptoMiniSat will use the modified version of cryptominisat.py. With this modification the ANF to CNF converter CNFEncoder produces the same CNF with CryptoMiniSat as with DIMACS as solver. And my example can be solved by sat.boolean_polynomials.solve().

Regards, Jörg.

hadipourh commented 5 years ago
comment:8

Dear Jörg,

I did as you said. It works for my example too. I think this modification solves the problem. I appreciate your time and efforts.

Sincerely, H. Hadipour

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago
comment:9

Great ! Should i go ahead and upload a branch with the fix (and doctests to avoid further regressions), or do you want to fix it yourself ?

jvpeetz commented 5 years ago
comment:10

Hi Thierry,

it's fine with me if you uploa d the fixes. As I mentioned this fix might also apply to the picosat binding.

By the way, thanks for making the newer version of CryptoMiniSat available in SageMath.

Regards, Jörg.

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago

Branch: u/tmonteil/fix_var_for_cryptominisat_and_picosat_solvers

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 5 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

c492724#26676 : add doctests for solving boolean polynomial systems with picosat
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 5 years ago

Commit: c492724

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago

Author: Thierry Monteil

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago

Changed keywords from solve_sat, CryptoMiniSat to solve_sat, CryptoMiniSat, picosat

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago
comment:13

I fixed the var() methods in cryptominisat and picosat and added the two examples you both provided as doctests to prevent future regressions with both solvers.

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago

Description changed:

--- 
+++ 
@@ -1 +1,4 @@
 When I used Sage7.2, I could easily solve my boolean equations with solve_sat commands, and it's results were verified by the papers and other tools, but when I upgraded my sage to version 8 (or later version) I found that the new solve_sat solver (especially when we use CryptoMiniSat as the SAT solver) doesn't work as correct as before. For example, when I solve a system of equations via solve_sat which used CryptoMiniSat as a SAT solver, I get different number of solutions in different version of [SageMath](../wiki/SageMath). I believe that there is something wrong in newer version of [SageMath](../wiki/SageMath) because my previous experiences shows that the older version's results were verified by the other tools and papers. I hope someone could solve this problem.
+
+See also the following thread on sage-devel: https://groups.google.com/forum/?fromgroups#!topic/sage-devel/2EhgHzGgUnQ
+
edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago
comment:15

Just to state the obvious: if nobody review this ticket, it will never get merged.

fchapoton commented 5 years ago
comment:16

ok

fchapoton commented 5 years ago

Reviewer: Frédéric Chapoton

vbraun commented 5 years ago

Changed branch from u/tmonteil/fix_var_for_cryptominisat_and_picosat_solvers to c492724