Visible to the public Biblio

Filters: Keyword is SAT  [Clear All Filters]
2022-06-09
Palit, Shekhar, Wortman, Kevin A..  2021.  Perfect Tabular Hashing in Pseudolinear Time. 2021 IEEE 11th Annual Computing and Communication Workshop and Conference (CCWC). :0228–0232.
We present an algorithm for generating perfect tabulation hashing functions by reduction to Boolean satisfaction (SAT). Tabulation hashing is a high-performance family of hash functions for hash tables that involves computing the XOR of random lookup tables. Given n keys of word size W, we show how to compute a perfect hash function in O(nW) worst-case time. This is competitive with other perfect hashing methods, and the resultant hash functions are simple and performant.
2020-11-09
Rao, V. V., Savidis, I..  2019.  Mesh Based Obfuscation of Analog Circuit Properties. 2019 IEEE International Symposium on Circuits and Systems (ISCAS). :1–5.
In this paper, a technique to design analog circuits with enhanced security is described. The proposed key based obfuscation technique uses a mesh topology to obfuscate the physical dimensions and the threshold voltage of the transistor. To mitigate the additional overhead of implementing the obfuscated circuitry, a satisfiability modulo theory (SMT) based algorithm is proposed to auto-determine the sizes of the transistors selected for obfuscation such that only a limited set of key values produce the correct circuit functionality. The proposed algorithm and the obfuscation methodology is implemented on an LC tank voltage-controlled oscillator (VCO). The operating frequency of the VCO is masked with a 24-bit encryption key applied to a 2×6 mesh structure that obfuscates the dimensions of each varactor transistor. The probability of determining the correct key is 5.96×10-8 through brute force attack. The dimensions of the obfuscated transistors determined by the analog satisfiability (aSAT) algorithm result in at least a 15%, 3%, and 13% deviation in, respectively, the effective transistor dimensions, target frequency, and voltage amplitude when an incorrect key is applied to the VCO. In addition, only one key produces the desired frequency and properly sets the overall performance specifications of the VCO. The simulated results indicate that the proposed design methodology, which quickly and accurately determines the transistor sizes for obfuscation, produces the target specifications and provides protection for analog circuits against IP piracy and reverse engineering.
2020-01-07
Matsunaga, Yusuke, Yoshimura, Masayoshi.  2019.  An Efficient SAT-Attack Algorithm Against Logic Encryption. 2019 IEEE 25th International Symposium on On-Line Testing and Robust System Design (IOLTS). :44-47.

This paper presents a novel efficient SAT-attack algorithm for logic encryption. The existing SAT-attack algorithm can decrypt almost all encrypted circuits proposed so far, however, there are cases that it takes a huge amount of CPU time. This is because the number of clauses being added during the decryption increases drastically in that case. To overcome that problem, a novel algorithm is developed, which considers the equivalence of clauses to be added. Experiments show that the proposed algorithm is much faster than the existing algorithm.

2017-09-15
Babenko, Ludmila, Maro, Ekaterina, Anikeev, Maxim.  2016.  Modeling of Algebraic Analysis of GOST+ Cipher in SageMath. Proceedings of the 9th International Conference on Security of Information and Networks. :100–103.

In this paper we present results of algebraic analysis of GOST⌖ algorithm in SageMath environment. Using the GOST⌖ as the example we explore basic stages of algebraic analysis of any symmetric block cipher based on Feistel network. We construct sets of boolean equations for five encryption rounds and determine the number of known text pairs for which the key can be found with the probability of 1. The algebraic analysis of five rounds of GOST⌖ allowed to find a 160-bit encryption key with the probability of 1 for five known text pairs within 797.21 s; the search for the solution took 24.66 s.