Abstract
Optimized and custom arithmetic circuits are widely used in embedded systems such as multimedia applications, cryptography systems, signal processing, and console games. Verification of arithmetic circuits is a challenge due to increasing complexity coupled with non-standard implementations. Existing algebraic rewriting techniques produce a remainder to indicate the presence of a potential Trojan. However, Trojan localization remains a major bottleneck. Simulation-based validation using random or constrained-random tests is not effective for complex arithmetic circuits due to bit-blasting. In this chapter, we present an automated test generation and Trojan localization technique for arithmetic circuits. We consider gate-replacement Trojan or signal inversion that changes the functionality of the design as the threat model. In this chapter, we present an automated approach for generating directed tests by suitable assignments of input variables to make the remainder non-zero. The generated tests are guaranteed to activate Trojans. We also present an automatic Trojan removal technique by utilizing the patterns of the remainder terms as well as by analyzing the regions activated by the generated tests to detect and correct the Trojan(s). We also present an efficient anomaly detection and correction algorithm that can handle multiple dependent as well as independent Trojans. This framework is capable of producing a corrected implementation of arithmetic circuits without any manual intervention. The experimental results demonstrate that the proposed approach can be used for automated anomaly detection and correction of large and complex arithmetic circuits.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
A. Ahmed, P. Mishra, QUEBS: qualifying event based search in concolic testing for validation of RTL models, in IEEE International Conference on Computer Design (ICCD) (2017), pp. 185–192
A. Ahmed, F. Farahmandi, P. Mishra, Directed test generation using concolic testing of RTL models, in Design Automation and Test in Europe (DATE), pp. 1538–1543 (2018)
E. Biham, Y. Carmeli, A. Shamir, Bug attacks, in Advances in Cryptology (2008), pp. 221–240
R.E. Bryant, Y.-A. Chen, Verification of arithmetic circuits with binary moment diagrams, in Proceedings of the 32nd Annual ACM/IEEE Design Automation Conference (ACM, New York, 1995), pp. 535–541
B. Buchberger, Some properties of gröbner-bases for polynomial ideals. ACM SIGSAM Bull. 10(4), 19–24 (1976)
B. Buchberger, A criterion for detecting unnecessary reductions in the construction of a Göbner bases, in EUROSAM (1979)
Cadence Berkeley Lab, The Cadence SMV Model Checker. Available at http://www.kenmcmil.com
M. Chen, P. Mishra, Functional test generation using efficient property clustering and learning techniques. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(3), 396–404 (2010)
M. Chen, P. Mishra, Property learning techniques for efficient generation of directed tests. IEEE Trans. Comput. 60(6), 852–864 (2011)
M. Chen, X. Qin, H. Koo, P. Mishra, System-level Validation – High-Level Modeling and Directed Test Generation Techniques (Springer, New York, 2012)
M. Chen, P. Mishra, D. Kalita, Automatic RTL test generation from SystemC TLM specifications. ACM Trans. Embed. Comput. Syst. 11(2), article 38 (2012)
M. Chen, X. Qin, P. Mishra, Learning-oriented property decomposition for automated generation of directed tests. J. Electron. Test. 30(3), 287–306 (2014)
M.J. Ciesielski, C. Yu, W. Brown, D. Liu, A. Rossi, Verification of gate-level arithmetic circuits by function extraction, in IEEE/ACM International Conference on Computer Design Automation(DAC) (2015), pp. 1–6
D. Cox, J. Little, D. O’shea, Ideals, Varieties, and Algorithms, vol. 3 (Springer, New York, 1992)
F. Farahmandi, B. Alizadeh, Gröbner basis based formal verification of large arithmetic circuits using Gaussian elimination and cone-based polynomial extraction, in Microprocessors and Microsystems – Embedded Hardware Design (2015), pp. 83–96
F. Farahmandi, P. Mishra, Automated test generation for debugging arithmetic circuits, in 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE) (IEEE, Piscataway, 2016), pp. 1351–1356
F. Farahmandi, P. Mishra, Automated debugging of arithmetic circuits using incremental Gröbner basis reduction, in 2017 IEEE 35th International Conference on Computer Design (ICCD) (IEEE, Piscataway, 2017), pp. 193–200
F. Farahmandi, P. Mishra, Automated test generation for debugging multiple bugs in arithmetic circuits. IEEE Trans. Comput. 68(2), 182–197 (2019)
F. Farahmandi, B. Alizadeh, Z. Navabi, Effective combination of algebraic techniques and decision diagrams to formally verify large arithmetic circuits, in 2014 IEEE Computer Society Annual Symposium on VLSI (IEEE, Piscataway, 2014), pp. 338–343
S. Ghandali, C. Yu, D. Liu, W. Brown, M. Ciesielski, Logic debugging of arithmetic circuits, in 2015 IEEE Computer Society Annual Symposium on VLSI (IEEE, Piscataway, 2015), pp. 113–118
G.-M. Greuel, G. Pfister, H. Schifinemann, SINGULAR 3.1.3 A computer algebra system for polynomial computations. Centre for Computer Algebra (2012). http://www.singular.uni-kl.de
M. Knežević, K. Sakiyama, J. Fan, I. Verbauwhed, Modular reduction in GF(2n) without pre-computational phase, in Proceedings of the International Workshop on Arithmetic of Finite Fields (2008), pp. 77–87
C. Koc, T. Acar, Montgomery multiplication in GF(2k), in Designs, Codes and Cryptography, vol. 14 (1998), pp. 57–69
H.-M. Koo, P. Mishra, Functional test generation using design and property decomposition techniques. ACM Trans. Embed. Comput. Syst. 8(4), article 32 (2009)
B. Le, H. Mangassarian, B. Keng, A. Veneris, Non-solution implications using reverse domination in a modern SAT-based debugging environment, in Design Automation and Test in Europe (DATE) (2012), pp. 629–634
J. Lv, P. Kalla, F. Enescu, Efficient Gröbner basis reductions for formal verification of Galois field multipliers, in Proceedings Design, Automation and Test in Europe Conference (DATE) (2012), pp. 899–904
J. Lv, P. Kalla, F. Enescu, Efficient Gröbner basis reductions for formal verification of Galois field arithmetic circuits. IEEE Trans. CAD 32, 1409–1420 (2013)
Y. Lyu, X. Qin, M. Chen, P. Mishra, Directed test generation for validation of cache coherence protocols. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 38, 163–176 (2018)
Y. Lyu, A. Ahmed, P. Mishra, Automated activation of multiple targets in RTL models using concolic testing, in Design Automation and Test in Europe (DATE) (2019)
H. Mangassarian, A. Veneris, S. Safarpour, M. Benedetti, D. Smith, A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test, in 2007 IEEE/ACM International Conference on Computer-Aided Design (IEEE, Piscataway, 2007), pp. 240–245
P. Mishra, N. Dutt, Specification-driven directed test generation for validation of pipelined processors. ACM Trans. Des. Autom. Electron. Syst. 13(2), 36 pp., article 42 (2008)
X. Qin, P. Mishra, Directed test generation for validation of multicore architectures. ACM Trans. Des. Autom. Electron. Syst. 17(3), article 24, 21 pp. (2012)
X. Qin, P. Mishra, Scalable test generation by interleaving concrete and symbolic execution, in International Conference on VLSI Design (2014), pp. 104–109
O. Wienand, M. Welder, D. Stoffel, W. Kunz, G.M. Greuel, An algebraic approach for proving data correctness in arithmetic data paths, in Computer Aided Verification (CAV) (2008), pp. 473–486
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Farahmandi, F., Huang, Y., Mishra, P. (2020). Anomaly Detection Using Symbolic Algebra. In: System-on-Chip Security. Springer, Cham. https://doi.org/10.1007/978-3-030-30596-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-30596-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30595-6
Online ISBN: 978-3-030-30596-3
eBook Packages: EngineeringEngineering (R0)