Computer Engineering Commons^™

Verification Of Transaction Ordering Dependence Vulnerability Of Smart Contract Based On Cpn, Hong Zheng, Zerun Liu, Jianhua Huang, Shihui Qian

Journal of System Simulation

Abstract: The formal verification of smart contracts researches mainly focus on programming language-level vulnerabilities, and the transaction ordering dependence is more difficult to be detected as a blockchain-level vulnerability.The latent transaction ordering dependence vulnerability in smart contracts is formally verified based on colored Petri nets.The latent vulnerability in the Decode reward contractis analyzed, anda colored Petri net model of the contract itself and its execution environment is established from top to bottom.The attacker model is introduced to consider the situation that the contract is attacked. By running the model to verify the existence of transaction ordering dependence vulnerability in …

Authentication And Sql-Injection Prevention Techniques In Web Applications, Cagri Cetin

USF Tampa Graduate Theses and Dissertations

This dissertation addresses the top two “most critical web-application security risks” by combining two high-level contributions.

The first high-level contribution introduces and evaluates collaborative authentication, or coauthentication, a single-factor technique in which multiple registered devices work together to authenticate a user. Coauthentication provides security benefits similar to those of multi-factor techniques, such as mitigating theft of any one authentication secret, without some of the inconveniences of multi-factor techniques, such as having to enter passwords or biometrics. Coauthentication provides additional security benefits, including: preventing phishing, replay, and man-in-the-middle attacks; basing authentications on high-entropy secrets that can be generated and updated automatically; …

Application Of Pwa-Based Safety Diagnosis Method In Cstr System, Yuhong Wang, Yang Pu

Journal of System Simulation

Abstract: A safety diagnosis method based on piecewise affine (PWA) model is proposed for ensuring the safety of the petrochemical process. In the method, the petrochemical system is modeled in PWA form which can well describe the nonlinear and hybrid characteristic of the system. Then a formal verification algorithm based on reachable analysis is used to get reachable sets of system states according to the established model. It can predict whether the system is in danger or not in advance so as to take the corresponding measures to ensure the reliability and safety of the system. The proposed method is …

A Memory-Efficient Canonical Data Structure For Decimal Floating Point Arithmetic Systems Modeling And Verification, Mohammad Saeed Jahangiry, Saeed Safari

Turkish Journal of Electrical Engineering and Computer Sciences

Decimal floating point (DFP) number representation was proposed in IEEE-754-2008 in order to overcome binary floating point inaccuracy. Neglecting binary floating point verification has resulted in significant validity and economic losses. Formal verification can be a solution to similar DFP design problems. Verification techniques aiming at DFP are limited to functional methods whereas formal approaches have been neglected and traditional decision diagrams cannot model DFP representation complexity. In this paper, we propose an efficient canonical data structure that can model DFP properties. Our novel data structure models coefficient, exponent, sign, and bias of a DFP number. We will prove mathematically …

Specification And Formal Verification Of Safety Properties In A Point Automation System, İbrahi̇m Şener, Özgür Turay Kaymakçi, İlker Üstoğlu, Gali̇p Cansever

Turkish Journal of Electrical Engineering and Computer Sciences

Railroad transportation systems are an area that poses the threat of causing huge risk for both the environment and people if an error emerges during operation. For this reason, designing and developing relevant products in this area is challenging. What is more, methods to be utilized for the purposes of minimizing risk susceptibility are to be specified by international standards. While relevant standards strongly recommend that some methods be utilized based on the desired safety integrity level during the development phase, some methods are not recommended to be utilized. CENELEC 50128 strongly recommends the utilization of timed-arc Petri nets during …