Biblio

The relevance of data protection is related to the intensive informatization of various aspects of society and the need to prevent unauthorized access to them. World spending on ensuring information security (IS) for the current state: expenses in the field of IS today amount to \$81.7 billion. Expenditure forecast by 2020: about \$105 billion [1]. Information protection of military facilities is the most critical in the public sector, in the non-state - financial organizations is one of the leaders in spending on information protection. An example of the importance of IS research is the Trojan encoder WannaCry, which infected hundreds of thousands of computers around the world, attacks are recorded in more than 116 countries. The attack of the encoder of WannaCry (Wana Decryptor) happens through a vulnerability in service Server Message Block (protocol of network access to file systems) of Windows OS. Then, a rootkit (a set of malware) was installed on the infected system, using which the attackers launched an encryption program. Then each vulnerable computer could become infected with another infected device within one local network. Due to these attacks, about \$70,000 was lost (according to data from 18.05.2017) [2]. It is assumed in the presented work, that the software level of information protection is fundamentally insufficient to ensure the stable functioning of critical objects. This is due to the possible hardware implementation of undocumented instructions, discussed later. The complexity of computing systems and the degree of integration of their components are constantly growing. Therefore, monitoring the operation of the computer hardware is necessary to achieve the maximum degree of protection, in particular, data processing methods.

Hardware vulnerabilities are often due to design mistakes because the designer does not sufficiently consider potential security vulnerabilities at the design stage. As a result, various security solutions have been developed to protect ICs, among which the language-based hardware security verification serves as a promising solution. The verification process will be performed while compiling the HDL of the design. However, similar to other formal verification methods, the language-based approach also suffers from scalability issue. Furthermore, existing solutions either lead to hardware overhead or are not designed for vulnerable or malicious logic detection. To alleviate these challenges, we propose a new language based framework, QIF-Verilog, to evaluate the trustworthiness of a hardware system at register transfer level (RTL). This framework introduces a quantified information flow (QIF) model and extends Verilog type systems to provide more expressiveness in presenting security rules; QIF is capable of checking the security rules given by the hardware designer. Secrets are labeled by the new type and then parsed to data flow, to which a QIF model will be applied. To demonstrate our approach, we design a compiler for QIF-Verilog and perform vulnerability analysis on benchmarks from Trust-Hub and OpenCore. We show that Trojans or design faults that leak information from circuit outputs can be detected automatically, and that our method evaluates the security of the design correctly.