From: Dejan Jovanovic Date: Thu, 8 May 2014 06:26:42 +0000 (-0700) Subject: Adding encoding of sha1 collision for the hashing example X-Git-Tag: cvc5-1.0.0~6922 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fdbc8e0582dfe1addb229d406201a2ec1d513959;p=cvc5.git Adding encoding of sha1 collision for the hashing example --- diff --git a/.cproject b/.cproject index 0e06c7a74..cd310c481 100644 --- a/.cproject +++ b/.cproject @@ -5,12 +5,12 @@ - + @@ -309,20 +309,21 @@ + - + make -j10 check true - false + true true - + make - -j10 - all + -j3 + true true true @@ -334,10 +335,10 @@ true true - + make -j10 - check + all true true true @@ -350,7 +351,14 @@ true true + + make + -j10 + check + true + false + true + - diff --git a/examples/hashsmt/Makefile.am b/examples/hashsmt/Makefile.am index b385856e7..21726e9a6 100644 --- a/examples/hashsmt/Makefile.am +++ b/examples/hashsmt/Makefile.am @@ -4,18 +4,28 @@ AM_CXXFLAGS = -Wall AM_CFLAGS = -Wall noinst_PROGRAMS = \ - sha1smt + sha1_inversion \ + sha1_collision noinst_DATA = -sha1smt_SOURCES = \ - sha1smt.cpp \ +sha1_inversion_SOURCES = \ + sha1_inversion.cpp \ word.h \ word.cpp \ sha1.hpp -sha1smt_LDADD = \ +sha1_inversion_LDADD = \ @builddir@/../../src/libcvc4.la +sha1_collision_SOURCES = \ + sha1_collision.cpp \ + word.h \ + word.cpp \ + sha1.hpp +sha1_collision_LDADD = \ + @builddir@/../../src/libcvc4.la + + # for installation examplesdir = $(docdir)/$(subdir) examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST) diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp index 0d4bbbf33..f033822c2 100644 --- a/examples/hashsmt/sha1.hpp +++ b/examples/hashsmt/sha1.hpp @@ -58,7 +58,7 @@ class sha1 public: typedef cvc4_uint32(&digest_type)[5]; public: - sha1(); + sha1(unsigned rounds = 80); void reset(); @@ -78,9 +78,12 @@ private: std::size_t block_byte_index_; std::size_t byte_count_; + + unsigned rounds_; }; -inline sha1::sha1() +inline sha1::sha1(unsigned rounds) +: rounds_(rounds) { reset(); } @@ -141,7 +144,7 @@ inline void sha1::process_block() cvc4_uint32 d = h_[3]; cvc4_uint32 e = h_[4]; - for (std::size_t i=0; i<80; ++i) { + for (std::size_t i=0; i +#include +#include +#include + +#include "word.h" +#include "sha1.hpp" +#include "expr/command.h" + +#include + +using namespace std; +using namespace CVC4; + +hashsmt::cvc4_uchar8 *createInput(unsigned size, std::string prefix, std::ostream& output) { + hashsmt::cvc4_uchar8 *input = new hashsmt::cvc4_uchar8[size]; + for(unsigned i = 0; i < size; ++i) { + stringstream ss; + ss << prefix << i; + input[i] = hashsmt::cvc4_uchar8(ss.str()); + output << DeclareFunctionCommand(ss.str(), input[i].getExpr(), input[i].getExpr().getType()) << endl; + } + return input; +} + +int main(int argc, char* argv[]) { + + try { + + // Check the arguments + if (argc != 4) { + cerr << "usage: sha1smt size rounds (1..80) output-file" << std::endl; + return 1; + } + + // Get the input size to encode + unsigned msgSize; + istringstream msgSize_is(argv[1]); + msgSize_is >> msgSize; + + // Get the number of rounds to use + unsigned rounds; + istringstream rounds_is(argv[2]); + rounds_is >> rounds; + + // The output + ofstream output(argv[3]); + output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2); + output << SetBenchmarkLogicCommand("QF_BV") << endl; + output << SetBenchmarkStatusCommand(SMT_UNSATISFIABLE) << endl; + + // Make the variables the size of the string + hashsmt::cvc4_uchar8 *cvc4input1 = createInput(msgSize, "x", output); + hashsmt::cvc4_uchar8 *cvc4input2 = createInput(msgSize, "y", output); + + // Do the cvc4 encoding for first message + hashsmt::sha1 cvc4encoder1(rounds); + cvc4encoder1.process_bytes(cvc4input1, msgSize); + hashsmt::cvc4_uint32 cvc4digest1[5]; + cvc4encoder1.get_digest(cvc4digest1); + + // Do the cvc4 encoding for second message + hashsmt::sha1 cvc4encoder2(rounds); + cvc4encoder2.process_bytes(cvc4input2, msgSize); + hashsmt::cvc4_uint32 cvc4digest2[5]; + cvc4encoder2.get_digest(cvc4digest2); + + // Create the assertion + Expr inputEqual = (hashsmt::Word::concat(cvc4input1, msgSize) == hashsmt::Word::concat(cvc4input2, msgSize)); + Expr digestEqual = (hashsmt::Word::concat(cvc4digest1, 5) == hashsmt::Word::concat(cvc4digest2, 5)); + Expr assertion = inputEqual.notExpr().andExpr(digestEqual); + + output << AssertCommand(assertion) << endl; + + // Checksat command + output << CheckSatCommand() << endl; + + } catch (CVC4::Exception& e) { + cerr << e << endl; + } +} + + + diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp new file mode 100644 index 000000000..720ef52b4 --- /dev/null +++ b/examples/hashsmt/sha1_inversion.cpp @@ -0,0 +1,107 @@ +/********************* */ +/*! \file sha1smt.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +/* + * sha1smt.cpp + * + * Created on: Jul 13, 2012 + * Author: dejan + */ + +#include +#include +#include +#include + +#include "word.h" +#include "sha1.hpp" +#include "expr/command.h" + +#include + +using namespace std; +using namespace CVC4; + +int main(int argc, char* argv[]) { + + try { + + // Check the arguments + if (argc != 3) { + cerr << "usage: sha1smt message output-file" << std::endl; + return 1; + } + + // Get the message to encode and the output file + string msg = argv[1]; + unsigned msgSize = msg.size(); + ofstream output(argv[2]); + output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2); + output << SetBenchmarkLogicCommand("QF_BV") << endl; + output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl; + + // Make the variables the size of the string + hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize]; + for (unsigned i = 0; i < msgSize; ++ i) { + stringstream ss; + ss << "x" << i; + cvc4input[i] = hashsmt::cvc4_uchar8(ss.str()); + output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl; + + // Ouput the solution also + Expr solution = (cvc4input[i] == hashsmt::cvc4_uchar8(msg.c_str()[i])); + output << "; " << AssertCommand(solution) << endl; + } + + // Do the cvc4 encoding + hashsmt::sha1 cvc4encoder; + cvc4encoder.process_bytes(cvc4input, msgSize); + + // Get the digest as bitvectors + hashsmt::cvc4_uint32 cvc4digest[5]; + cvc4encoder.get_digest(cvc4digest); + + // Do the actual sha1 encoding + boost::uuids::detail::sha1 sha1encoder; + sha1encoder.process_bytes(msg.c_str(), msgSize); + unsigned sha1digest[5]; + sha1encoder.get_digest(sha1digest); + + // Create the assertion + Expr assertion; + for (unsigned i = 0; i < 5; ++ i) { + Expr conjunct = (cvc4digest[i] == hashsmt::cvc4_uint32(sha1digest[i])); + if (i > 0) { + assertion = assertion.andExpr(conjunct); + } else { + assertion = conjunct; + } + } + output << AssertCommand(assertion) << endl; + + // Checksat command + output << CheckSatCommand() << endl; + + delete cvc4input; + + } catch (CVC4::Exception& e) { + cerr << e << endl; + } +} + + + diff --git a/examples/hashsmt/sha1smt.cpp b/examples/hashsmt/sha1smt.cpp deleted file mode 100644 index 720ef52b4..000000000 --- a/examples/hashsmt/sha1smt.cpp +++ /dev/null @@ -1,107 +0,0 @@ -/********************* */ -/*! \file sha1smt.cpp - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/* - * sha1smt.cpp - * - * Created on: Jul 13, 2012 - * Author: dejan - */ - -#include -#include -#include -#include - -#include "word.h" -#include "sha1.hpp" -#include "expr/command.h" - -#include - -using namespace std; -using namespace CVC4; - -int main(int argc, char* argv[]) { - - try { - - // Check the arguments - if (argc != 3) { - cerr << "usage: sha1smt message output-file" << std::endl; - return 1; - } - - // Get the message to encode and the output file - string msg = argv[1]; - unsigned msgSize = msg.size(); - ofstream output(argv[2]); - output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2); - output << SetBenchmarkLogicCommand("QF_BV") << endl; - output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl; - - // Make the variables the size of the string - hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize]; - for (unsigned i = 0; i < msgSize; ++ i) { - stringstream ss; - ss << "x" << i; - cvc4input[i] = hashsmt::cvc4_uchar8(ss.str()); - output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl; - - // Ouput the solution also - Expr solution = (cvc4input[i] == hashsmt::cvc4_uchar8(msg.c_str()[i])); - output << "; " << AssertCommand(solution) << endl; - } - - // Do the cvc4 encoding - hashsmt::sha1 cvc4encoder; - cvc4encoder.process_bytes(cvc4input, msgSize); - - // Get the digest as bitvectors - hashsmt::cvc4_uint32 cvc4digest[5]; - cvc4encoder.get_digest(cvc4digest); - - // Do the actual sha1 encoding - boost::uuids::detail::sha1 sha1encoder; - sha1encoder.process_bytes(msg.c_str(), msgSize); - unsigned sha1digest[5]; - sha1encoder.get_digest(sha1digest); - - // Create the assertion - Expr assertion; - for (unsigned i = 0; i < 5; ++ i) { - Expr conjunct = (cvc4digest[i] == hashsmt::cvc4_uint32(sha1digest[i])); - if (i > 0) { - assertion = assertion.andExpr(conjunct); - } else { - assertion = conjunct; - } - } - output << AssertCommand(assertion) << endl; - - // Checksat command - output << CheckSatCommand() << endl; - - delete cvc4input; - - } catch (CVC4::Exception& e) { - cerr << e << endl; - } -} - - - diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp index ac9cfbcff..3035983d9 100644 --- a/examples/hashsmt/word.cpp +++ b/examples/hashsmt/word.cpp @@ -24,6 +24,8 @@ #include "word.h" +#include + using namespace std; using namespace hashsmt; using namespace CVC4; @@ -55,6 +57,14 @@ Expr Word::operator == (const Word& b) const { return em()->mkExpr(kind::EQUAL, d_expr, b.getExpr()); } +Word Word::concat(const Word words[], unsigned size) { + Expr concat = words[0].d_expr; + for(unsigned i = 1; i < size; ++i) { + concat = em()->mkExpr(kind::BITVECTOR_CONCAT, concat, words[i].d_expr); + } + return Word(concat); +} + void Word::print(ostream& out) const { out << CVC4::Expr::setdepth(-1) << d_expr; } diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h index f8c03f7b2..dd1c2dc38 100644 --- a/examples/hashsmt/word.h +++ b/examples/hashsmt/word.h @@ -79,6 +79,9 @@ public: /** Returns the comparison expression */ CVC4::Expr operator == (const Word& b) const; + + /** Concatenate the given words */ + static Word concat(const Word words[], unsigned size); }; inline std::ostream& operator << (std::ostream& out, const Word& word) {