Visible to the public Biblio

Filters: Keyword is process control  [Clear All Filters]
2020-11-17
Poltronieri, F., Sadler, L., Benincasa, G., Gregory, T., Harrell, J. M., Metu, S., Moulton, C..  2018.  Enabling Efficient and Interoperable Control of IoBT Devices in a Multi-Force Environment. MILCOM 2018 - 2018 IEEE Military Communications Conference (MILCOM). :757—762.

Efficient application of Internet of Battlefield Things (IoBT) technology on the battlefield calls for innovative solutions to control and manage the deluge of heterogeneous IoBT devices. This paper presents an innovative paradigm to address heterogeneity in controlling IoBT and IoT devices, enabling multi-force cooperation in challenging battlefield scenarios.

2020-11-09
Islam, S. A., Sah, L. K., Katkoori, S..  2019.  DLockout: A Design Lockout Technique for Key Obfuscated RTL IP Designs. 2019 IEEE International Symposium on Smart Electronic Systems (iSES) (Formerly iNiS). :17–20.
Intellectual Property (IP) infringement including piracy and overproduction have emerged as significant threats in the semiconductor supply chain. Key-based obfuscation techniques (i.e., logic locking) are widely applied to secure legacy IP from such attacks. However, the fundamental question remains open whether an attacker is allowed an exponential amount of time to seek correct key or could it be useful to lock out the design in a non-destructive manner after several incorrect attempts. In this paper, we address this question with a robust design lockout technique. Specifically, we perform comparisons on obfuscation logic output that reflects the condition (correct or incorrect) of the applied key without changing the system behavior. The proposed approach, when combined with key obfuscation (logic locking) technique, increases the difficulty of reverse engineering key obfuscated RTL module. We provide security evaluation of DLockout against three common side-channel attacks followed by a quantitative assessment of the resilience. We conducted a set of experiments on four datapath intensive IPs and one crypto core for three different key lengths (32-, 64-, and 128-bit) under the typical design corner. On average, DLockout incurs negligible area, power, and delay overheads.
2020-11-02
Bloom, Gedare, Alsulami, Bassma, Nwafor, Ebelechukwu, Bertolotti, Ivan Cibrario.  2018.  Design patterns for the industrial Internet of Things. 2018 14th IEEE International Workshop on Factory Communication Systems (WFCS). :1—10.
The Internet of Things (IoT) is a vast collection of interconnected sensors, devices, and services that share data and information over the Internet with the objective of leveraging multiple information sources to optimize related systems. The technologies associated with the IoT have significantly improved the quality of many existing applications by reducing costs, improving functionality, increasing access to resources, and enhancing automation. The adoption of IoT by industries has led to the next industrial revolution: Industry 4.0. The rise of the Industrial IoT (IIoT) promises to enhance factory management, process optimization, worker safety, and more. However, the rollout of the IIoT is not without significant issues, and many of these act as major barriers that prevent fully achieving the vision of Industry 4.0. One major area of concern is the security and privacy of the massive datasets that are captured and stored, which may leak information about intellectual property, trade secrets, and other competitive knowledge. As a way forward toward solving security and privacy concerns, we aim in this paper to identify common input-output (I/O) design patterns that exist in applications of the IIoT. These design patterns enable constructing an abstract model representation of data flow semantics used by such applications, and therefore better understand how to secure the information related to IIoT operations. In this paper, we describe communication protocols and identify common I/O design patterns for IIoT applications with an emphasis on data flow in edge devices, which, in the industrial control system (ICS) setting, are most often involved in process control or monitoring.
2020-10-05
Zamani, Majid, Arcak, Murat.  2018.  Compositional Abstraction for Networks of Control Systems: A Dissipativity Approach. IEEE Transactions on Control of Network Systems. 5:1003—1015.

In this paper, we propose a compositional scheme for the construction of abstractions for networks of control systems by using the interconnection matrix and joint dissipativity-type properties of subsystems and their abstractions. In the proposed framework, the abstraction, itself a control system (possibly with a lower dimension), can be used as a substitution of the original system in the controller design process. Moreover, we provide a procedure for constructing abstractions of a class of nonlinear control systems by using the bounds on the slope of system nonlinearities. We illustrate the proposed results on a network of linear control systems by constructing its abstraction in a compositional way without requiring any condition on the number or gains of the subsystems. We use the abstraction as a substitute to synthesize a controller enforcing a certain linear temporal logic specification. This example particularly elucidates the effectiveness of dissipativity-type compositional reasoning for large-scale systems.

Xue, Baoze, Shen, Pubing, Wu, Bo, Wang, Xiaoting, Chen, Shuwen.  2019.  Research on Security Protection of Network Based on Address Layout Randomization from the Perspective of Attackers. 2019 IEEE 8th Joint International Information Technology and Artificial Intelligence Conference (ITAIC). :1475–1478.
At present, the network architecture is based on the TCP/IP protocol and node communications are achieved by the IP address and identifier of the node. The IP address in the network remains basically unchanged, so it is more likely to be attacked by network intruder. To this end, it is important to make periodic dynamic hopping in a specific address space possible, so that an intruder fails to obtain the internal network address and grid topological structure in real time and to continue to perform infiltration by the building of a new address space layout randomization system on the basis of SDN from the perspective of an attacker.
2020-09-04
Mahmood, Riyadh Zaghlool, Fathil, Ahmed Fehr.  2019.  High Speed Parallel RC4 Key Searching Brute Force Attack Based on FPGA. 2019 International Conference on Advanced Science and Engineering (ICOASE). :129—134.
A parallel brute force attack on RC4 algorithm based on FPGA (Field Programmable Gate Array) with an efficient style has been presented. The main idea of this design is to use number of forecast keying methods to reduce the overall clock pulses required depended to key searching operation by utilizes on-chip BRAMs (block RAMs) of FPGA for maximizing the total number of key searching unit with taking into account the highest clock rate. Depending on scheme, 32 key searching units and main controller will be used in one Xilinx XC3S1600E-4 FPGA device, all these units working in parallel and each unit will be searching in a specific range of keys, by comparing the current result with the well-known cipher text if its match the found flag signal will change from 0 to 1 and the main controller will receive this signal and stop the searching operation. This scheme operating at 128-MHz clock frequency and gives us key searching speed of 7.7 × 106 keys/sec. Testing all possible keys (40-bits length), requires only around 39.5h.
2020-07-24
CUI, A-jun, Fu, Jia-yu, Wang, Wei, Zhang, Hua-feng.  2019.  Construction of Network Active Security Threat Model Based on Offensive and Defensive Differential Game. 2019 12th International Conference on Intelligent Computation Technology and Automation (ICICTA). :289—294.
Aiming at the shortcomings of the traditional network active security threat model that cannot continuously control the threat process, a network active security threat model based on offensive and defensive differential game is constructed. The attack and defense differential game theory is used to define the parameters of the network active security threat model, on this basis, the network security target is determined, the network active security threat is identified by the attack defense differential equation, and finally the network active security threat is quantitatively evaluated, thus construction of network active security threat model based on offensive and defensive differential game is completed. The experimental results show that compared with the traditional network active security threat model, the proposed model is more feasible in the attack and defense control of the network active security threat process, and can achieve the ideal application effect.
Chernov, Denis, Sychugov, Alexey.  2019.  Development of a Mathematical Model of Threat to Information Security of Automated Process Control Systems. 2019 International Russian Automation Conference (RusAutoCon). :1—5.
The authors carry out the analysis of the process of modeling threats to information security of automated process control systems. Basic principles of security threats model formation are considered. The approach to protection of automated process control systems based on the Shtakelberg game in a strategic form was modeled. An abstract mathematical model of information security threats to automated process control systems was developed. A formalized representation of a threat model is described, taking into account an intruder's potential. Presentation of the process of applying the described threat model in the form of a continuous Deming-Shewhart cycle is proposed.
2020-06-08
Sahabandu, Dinuka, Moothedath, Shana, Bushnell, Linda, Poovendran, Radha, Aller, Joey, Lee, Wenke, Clark, Andrew.  2019.  A Game Theoretic Approach for Dynamic Information Flow Tracking with Conditional Branching. 2019 American Control Conference (ACC). :2289–2296.
In this paper, we study system security against Advanced Persistent Threats (APTs). APTs are stealthy and persistent but APTs interact with system and introduce information flows in the system as data-flow and control-flow commands. Dynamic Information Flow Tracking (DIFT) is a promising detection mechanism against APTs which taints suspicious input sources in the system and performs online security analysis when a tainted information is used in unauthorized manner. Our objective in this paper is to model DIFT that handle data-flow and conditional branches in the program that arise from control-flow commands. We use game theoretic framework and provide the first analytical model of DIFT with data-flow and conditional-branch tracking. Our game model which is an undiscounted infinite-horizon stochastic game captures the interaction between APTs and DIFT and the notion of conditional branching. We prove that the best response of the APT is a maximal reachability probability problem and provide a polynomial-time algorithm to find the best response by solving a linear optimization problem. We formulate the best response of the defense as a linear optimization problem and show that an optimal solution to the linear program returns a deterministic optimal policy for the defense. Since finding Nash equilibrium for infinite-horizon undiscounted stochastic games is computationally difficult, we present a nonlinear programming based polynomial-time algorithm to find an E-Nash equilibrium. Finally, we perform experimental analysis of our algorithm on real-world data for NetRecon attack augmented with conditional branching.
2020-05-18
Han, Ying, Li, Kun, Ge, Fawei.  2019.  Multiple Fault Diagnosis for Sucker Rod Pumping Systems Based on Matter Element Analysis with F-statistics. 2019 IEEE 8th Data Driven Control and Learning Systems Conference (DDCLS). :66–70.
Dynamometer cards can reflect different down-hole working conditions of sucker rod pumping wells. It has great significances to realize multiple fault diagnosis for actual oilfield production. In this paper, the extension theory is used to build a matter-element model to describe the fault diagnosis problem of the sucker rod pumping wells. The correlation function is used to calculate the correlation degree between the diagnostic fault and many standard fault types. The diagnosed sample and many possible fault types are divided into different combinations according to the correlation degree; the F-statistics of each combination is calculated and the “unbiased transformation” is used to find the mean of interval vectors. Larger F-statistics means greater differences within the faults classification; and the minimum F-statistics reflects the real multiple fault types. Case study shows the effectiveness of the proposed method.
2020-05-15
Khorsandroo, Sajad, Tosun, Ali Saman.  2018.  Time Inference Attacks on Software Defined Networks: Challenges and Countermeasures. 2018 IEEE 11th International Conference on Cloud Computing (CLOUD). :342—349.

Through time inference attacks, adversaries fingerprint SDN controllers, estimate switches flow-table size, and perform flow state reconnaissance. In fact, timing a SDN and analyzing its results can expose information which later empowers SDN resource-consumption or saturation attacks. In the real world, however, launching such attacks is not easy. This is due to some challenges attackers may encounter while attacking an actual SDN deployment. These challenges, which are not addressed adequately in the related literature, are investigated in this paper. Accordingly, practical solutions to mitigate such attacks are also proposed. Discussed challenges are clarified by means of conducting extensive experiments on an actual cloud data center testbed. Moreover, mitigation schemes have been implemented and examined in details. Experimental results show that proposed countermeasures effectively block time inference attacks.

2020-05-11
Kinkelin, Holger, Hauner, Valentin, Niedermayer, Heiko, Carle, Georg.  2018.  Trustworthy configuration management for networked devices using distributed ledgers. NOMS 2018 - 2018 IEEE/IFIP Network Operations and Management Symposium. :1–5.
Numerous IoT applications, like building automation or process control of industrial sites, exist today. These applications inherently have a strong connection to the physical world. Hence, IT security threats cannot only cause problems like data leaks but also safety issues which might harm people. Attacks on IT systems are not only performed by outside attackers but also insiders like administrators. For this reason, we present ongoing work on a Byzantine fault tolerant configuration management system (CMS) that provides control over administrators, restrains their rights, and enforces separation of concerns. We reach this goal by conducting a configuration management process that requires multi-party authorization for critical configurations to prevent individual malicious administrators from performing undesired actions. Only after a configuration has been authorized by multiple experts, it is applied to the targeted devices. For the whole configuration management process, our CMS guarantees accountability and traceability. Lastly, our system is tamper-resistant as we leverage Hyperledger Fabric, which provides a distributed execution environment for our CMS and a blockchain-based distributed ledger that we use to store the configurations. A beneficial side effect of this approach is that our CMS is also suitable to manage configurations for infrastructure shared across different organizations that do not need to trust each other.
2020-05-08
Lavrova, Daria, Zegzhda, Dmitry, Yarmak, Anastasiia.  2019.  Using GRU neural network for cyber-attack detection in automated process control systems. 2019 IEEE International Black Sea Conference on Communications and Networking (BlackSeaCom). :1—3.
This paper provides an approach to the detection of information security breaches in automated process control systems (APCS), which consists in forecasting multivariate time series formed from the values of the operating parameters of the end system devices. Using an experimental model of water treatment, a comparison was made of the forecasting results for the parameters characterizing the operation of the entire model, and for the parameters characterizing the flow of individual subprocesses implemented by the model. For forecasting, GRU-neural network training was performed.
2020-04-10
Watanabe, Hidenobu, Kondo, Tohru, Ohigashi, Toshihiro.  2019.  Implementation of Platform Controller and Process Modules of the Edge Computing for IoT Platform. 2019 IEEE International Conference on Pervasive Computing and Communications Workshops (PerCom Workshops). :407—410.
Edge computing requires a flexible choice of data-processing and rapidly computation performed at the edge of networks. We proposed an edge computing platform with container-based virtualization technology. In the platform, data-processing instances are modularized and deployed to edge nodes suitable for user requirements with keeping the data-processing flows within wide area network. This paper reports the platform controller and the process modules implemented to realize the secure and flexible edge computing platform.
2020-03-23
Tejendra, D.S., Varunkumar, C.R., Sriram, S.L., Sumathy, V., Thejeshwari, C.K..  2019.  A Novel Approach to reduce Vulnerability on Router by Zero vulnerability Encrypted password in Router (ZERO) Mechanism. 2019 3rd International Conference on Computing and Communications Technologies (ICCCT). :163–167.
As technology is developing exponentially and the world is moving towards automation, the resources have to be transferred through the internet which requires routers to connect networks and forward bundles (information). Due to the vulnerability of routers the data and resources have been hacked. The vulnerability of routers is due to minimum authentication to the network shared, some technical attacks on routers, leaking of passwords to others, single passwords. Based on the study, the solution is to maximize authentication of the router by embedding an application that monitors the user entry based on MAC address of the device, the password is frequently changed and that encrypted password is sent to a user and notifies the admin about the changes. Thus, these routers provide high-level security to the forward data through the internet.
2020-03-16
Radoglou-Grammatikis, Panagiotis, Sarigiannidis, Panagiotis, Giannoulakis, Ioannis, Kafetzakis, Emmanouil, Panaousis, Emmanouil.  2019.  Attacking IEC-60870-5-104 SCADA Systems. 2019 IEEE World Congress on Services (SERVICES). 2642-939X:41–46.
The rapid evolution of the Information and Communications Technology (ICT) services transforms the conventional electrical grid into a new paradigm called Smart Grid (SG). Even though SG brings significant improvements, such as increased reliability and better energy management, it also introduces multiple security challenges. One of the main reasons for this is that SG combines a wide range of heterogeneous technologies, including Internet of Things (IoT) devices as well as Supervisory Control and Data Acquisition (SCADA) systems. The latter are responsible for monitoring and controlling the automatic procedures of energy transmission and distribution. Nevertheless, the presence of these systems introduces multiple vulnerabilities because their protocols do not implement essential security mechanisms such as authentication and access control. In this paper, we focus our attention on the security issues of the IEC 60870-5-104 (IEC-104) protocol, which is widely utilized in the European energy sector. In particular, we provide a SCADA threat model based on a Coloured Petri Net (CPN) and emulate four different types of cyber attacks against IEC-104. Last, we used AlienVault's risk assessment model to evaluate the risk level that each of these cyber attacks introduces to our system to confirm our intuition about their severity.
Lin, Kuo-Sui.  2019.  A New Evaluation Model for Information Security Risk Management of SCADA Systems. 2019 IEEE International Conference on Industrial Cyber Physical Systems (ICPS). :757–762.
Supervisory control and data acquisition (SCADA) systems are becoming increasingly susceptible to cyber-physical attacks on both physical and cyber layers of critical information infrastructure. Failure Mode and Effects Analysis (FMEA) have been widely used as a structured method to prioritize all possible vulnerable areas (failure modes) for design review of security of information systems. However, traditional RPN based FMEA has some inherent problems. Besides, there is a lacking of application of FMEA for security in SCADAs under vague and uncertain environment. Thus, the main purpose of this study was to propose a new evaluation model, which not only intends to recover above mentioned problems, but also intends to evaluate, prioritize and correct security risk of SCADA system's threat modes. A numerical case study was also conducted to demonstrate that the proposed new evaluation model is not only capable of addressing FMEA's inherent problems but also is best suited for a semi-quantitative high level analysis of a secure SCADA's failure modes in the early design phases.
2020-02-26
Almohaimeed, Abdulrahman, Asaduzzaman, Abu.  2019.  Incorporating Monitoring Points in SDN to Ensure Trusted Links Against Misbehaving Traffic Flows. 2019 Fifth Conference on Mobile and Secure Services (MobiSecServ). :1–4.

The growing trend toward information technology increases the amount of data travelling over the network links. The problem of detecting anomalies in data streams has increased with the growth of internet connectivity. Software-Defined Networking (SDN) is a new concept of computer networking that can adapt and support these growing trends. However, the centralized nature of the SDN design is challenged by the need for an efficient method for traffic monitoring against traffic anomalies caused by misconfigured devices or ongoing attacks. In this paper, we propose a new model for traffic behavior monitoring that aims to ensure trusted communication links between the network devices. The main objective of this model is to confirm that the behavior of the traffic streams matches the instructions provided by the SDN controller, which can help to increase the trust between the SDN controller and its covered infrastructure components. According to our preliminary implementation, the behavior monitoring unit is able to read all traffic information and perform a validation process that reports any mismatching traffic to the controller.

2020-02-17
Hadar, Ethan, Hassanzadeh, Amin.  2019.  Big Data Analytics on Cyber Attack Graphs for Prioritizing Agile Security Requirements. 2019 IEEE 27th International Requirements Engineering Conference (RE). :330–339.

In enterprise environments, the amount of managed assets and vulnerabilities that can be exploited is staggering. Hackers' lateral movements between such assets generate a complex big data graph, that contains potential hacking paths. In this vision paper, we enumerate risk-reduction security requirements in large scale environments, then present the Agile Security methodology and technologies for detection, modeling, and constant prioritization of security requirements, agile style. Agile Security models different types of security requirements into the context of an attack graph, containing business process targets and critical assets identification, configuration items, and possible impacts of cyber-attacks. By simulating and analyzing virtual adversary attack paths toward cardinal assets, Agile Security examines the business impact on business processes and prioritizes surgical requirements. Thus, handling these requirements backlog that are constantly evaluated as an outcome of employing Agile Security, gradually increases system hardening, reduces business risks and informs the IT service desk or Security Operation Center what remediation action to perform next. Once remediated, Agile Security constantly recomputes residual risk, assessing risk increase by threat intelligence or infrastructure changes versus defender's remediation actions in order to drive overall attack surface reduction.

2020-01-20
He, Zecheng, Raghavan, Aswin, Hu, Guangyuan, Chai, Sek, Lee, Ruby.  2019.  Power-Grid Controller Anomaly Detection with Enhanced Temporal Deep Learning. 2019 18th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/13th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). :160–167.
Controllers of security-critical cyber-physical systems, like the power grid, are a very important class of computer systems. Attacks against the control code of a power-grid system, especially zero-day attacks, can be catastrophic. Earlier detection of the anomalies can prevent further damage. However, detecting zero-day attacks is extremely challenging because they have no known code and have unknown behavior. Furthermore, if data collected from the controller is transferred to a server through networks for analysis and detection of anomalous behavior, this creates a very large attack surface and also delays detection. In order to address this problem, we propose Reconstruction Error Distribution (RED) of Hardware Performance Counters (HPCs), and a data-driven defense system based on it. Specifically, we first train a temporal deep learning model, using only normal HPC readings from legitimate processes that run daily in these power-grid systems, to model the normal behavior of the power-grid controller. Then, we run this model using real-time data from commonly available HPCs. We use the proposed RED to enhance the temporal deep learning detection of anomalous behavior, by estimating distribution deviations from the normal behavior with an effective statistical test. Experimental results on a real power-grid controller show that we can detect anomalous behavior with high accuracy (\textbackslashtextgreater99.9%), nearly zero false positives and short (\textbackslashtextless; 360ms) latency.
2020-01-13
Zegzhda, Dmitry, Lavrova, Daria, Khushkeev, Aleksei.  2019.  Detection of information security breaches in distributed control systems based on values prediction of multidimensional time series. 2019 IEEE International Conference on Industrial Cyber Physical Systems (ICPS). :780–784.
Proposed an approach for information security breaches detection in distributed control systems based on prediction of multidimensional time series formed of sensor and actuator data.
2020-01-02
Shabanov, Boris, Sotnikov, Alexander, Palyukh, Boris, Vetrov, Alexander, Alexandrova, Darya.  2019.  Expert System for Managing Policy of Technological Security in Uncertainty Conditions: Architectural, Algorithmic, and Computing Aspects. 2019 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering (EIConRus). :1716–1721.

The paper discusses the architectural, algorithmic and computing aspects of creating and operating a class of expert system for managing technological safety of an enterprise, in conditions of a large flow of diagnostic variables. The algorithm for finding a faulty technological chain uses expert information, formed as a set of evidence on the influence of diagnostic variables on the correctness of the technological process. Using the Dempster-Schafer trust function allows determining the overall probability measure on subsets of faulty process chains. To combine different evidence, the orthogonal sums of the base probabilities determined for each evidence are calculated. The procedure described above is converted into the rules of the knowledge base production. The description of the developed prototype of the expert system, its architecture, algorithmic and software is given. The functionality of the expert system and configuration tools for a specific type of production are under discussion.

2019-12-16
Sayin, Muhammed O., Ba\c sar, Tamer.  2018.  Secure Sensor Design for Resiliency of Control Systems Prior to Attack Detection. 2018 IEEE Conference on Control Technology and Applications (CCTA). :1686-1691.

We introduce a new defense mechanism for stochastic control systems with control objectives, to enhance their resilience before the detection of any attacks. To this end, we cautiously design the outputs of the sensors that monitor the state of the system since the attackers need the sensor outputs for their malicious objectives in stochastic control scenarios. Different from the defense mechanisms that seek to detect infiltration or to improve detectability of the attacks, the proposed approach seeks to minimize the damage of possible attacks before they actually have even been detected. We, specifically, consider a controlled Gauss-Markov process, where the controller could have been infiltrated into at any time within the system's operation. Within the framework of game-theoretic hierarchical equilibrium, we provide a semi-definite programming based algorithm to compute the optimal linear secure sensor outputs that enhance the resiliency of control systems prior to attack detection.

2019-12-02
Tseng, Yuchia, Nait-Abdesselam, Farid, Khokhar, Ashfaq.  2018.  SENAD: Securing Network Application Deployment in Software Defined Networks. 2018 IEEE International Conference on Communications (ICC). :1–6.
The Software Defined Networks (SDN) paradigm, often referred to as a radical new idea in networking, promises to dramatically simplify network management by enabling innovation through network programmability. However, notable security issues, such as app-to-control threats, remain a significant concern that impedes SDN from being widely adopted. To cope with those app-to-control threats, this paper proposes a solution to securely deploy valid network applications while protecting the SDN controller against the injection of the malicious application. This problem is mitigated by proposing a novel SDN architecture, dubbed SENAD, which splits the well-known SDN controller into: (1) a data plane controller (DPC), and (2) an application plane controller (APC), to secure this latter by design. The role of the DPC is dedicated for interpreting the network rules into OpenFlow entries and maintaining the communication with the data plane. The role of the APC, however, is to provide a secured runtime for deploying the network applications, including authentication, access control, resource isolation, control, and monitoring applications. We show that this approach can easily shield against any deny of service, caused for instance by the resource exhaustion attack or the malicious command injection, that is caused by the co-existence of a malicious application on the controller's runtime. The evaluation of our architecture shows that the packet\_in messages take less than 5 ms to be delivered from the data plane to the application plane on the long range.
2019-11-12
Hu, Yayun, Li, Dongfang.  2019.  Formal Verification Technology for Asynchronous Communication Protocol. 2019 IEEE 19th International Conference on Software Quality, Reliability and Security Companion (QRS-C). :482-486.

For aerospace FPGA software products, traditional simulation method faces severe challenges to verify product requirements under complicated scenarios. Given the increasing maturity of formal verification technology, this method can significantly improve verification work efficiency and product design quality, by expanding coverage on those "blind spots" in product design which were not easily identified previously. Taking UART communication as an example, this paper proposes several critical points to use formal verification for asynchronous communication protocol. Experiments and practices indicate that formal verification for asynchronous communication protocol can effectively reduce the time required, ensure a complete verification process and more importantly, achieve more accurate and intuitive results.