Formal Methods for Approximate Computing in Arithmetic Circuits and Hardware-Accelerated Network Traffic Filtering
The talk covers two recent results where formal methods were used to approximate different computing tasks. Namely, we start with a presentation of an approach that combines genetic algorithms and formal verification to obtain approximations of arithmetic circuits (multipliers, adders, multiply-accumulate circuits, etc.) that trade some precision for a much smaller size and power consumption of the circuits. Such approximate circuits are very well suitable for various tasks (e.g., in data mining, image filtering, or machine learning) where exact computations are not needed. Still, it is usually good if the error stays within some bounds, which the use of formal methods can guarantee. In the second part of the talk, we will briefly touch upon another application of formal methods for approximate computing. In this case, we will speak about approximate reduction of non-deterministic finite automata used in hardware-accelerated network traffic filtering (aimed, e.g., at filtering out network attacks). For the price of changing the language of the automata, the proposed approach can squeeze the size of the automata much more than classical language-preserving reductions. Consequently, it is possible to use the current FPGA technology for FPGA-accelerated filtering at speeds of 100–400 Gbps while keeping the misclassification ratio rather low on real traffic.
The talk is based on the following papers and it is a result of collaboration with the co-authors of these papers:
* M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar. Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished. In Proc. of 36th International Conference On Computer Aided Design---ICCAD’17, IEEE CS, 2017. A bronze medal in the 2018 Human-Competitive Awards: "Humies”.
* M. Ceska, V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. In Proc. of 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'18, LNCS 10806, Springer-Verlag, 2018.
* M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar. ADAC: Automated Design of Approximate Circuits. Inn Proc. of 30th International Conference on Computer Aided Verification---CAV'18, LNCS 10981, Springer-Verlag, 2018.
17/10/2018 12:00
Computer Systems
Tomas Vojnar (http://www.fit.vutbr.cz/~vojnar/) received his PhD degree at Brno University of Technology (BUT) in the Czech Republic in 2001. From 2001 to 2003, he was a postdoc researcher at LIAFA (now IRIF), University Paris Diderot/Paris 7. He then returned to BUT where he holds a position of a full professor since 2012. His research includes automated formal analysis and verification, dynamic analysis and testing, as well as efficient ways of dealing with automata and logics with applications going beyond analysis and verification.
He published over 120 scientific publications in various journals and conferences (including venues such as TACAS, CAV, POPL, ICCAD, ATVA, SAS, ICST, or ISSTA). He was involved in a number of Czech as well as European projects. Currently, he is the coordinator of the Czech consortium within the H2020 ECSEL project Aquas.
The works he co-authored received the EATCS best theory paper award at TACAS'10, the best tool paper awards at RV'12 and ISSTA‘18, the Goedel medal at FLoC‘14 in Vienna, and won 11 medals (including 7 gold medals) with the Predator tool at the international software verification competition SV-COMP. In 2019, he is going to serve as a PC co-chair of TACAS 2019.
