Mutation-based fuzzing has been widely used in both academia and industry. Recently, researchers observe that the mutation scheduling scheme affects the efficiency of fuzzing. Accordingly, they propose PSO algorithm or machine learning-based technique to optimize the scheduling process. However, these methods fail to consider the fact that the optimal operator distribution of different seeds is different, even for the same program. In this paper, we propose a novel general scheduling scheme, named FA-fuzz, to find the optimal selecting probability distribution of mutation operators, which is based on the observations that the effective mutation operators are different for different seeds. Specifically, our method is based on the firefly algorithm. The positions of fireflies are mapped to the selection probability distribution of different mutation operators. The brightness of fireflies is expressed as the efficiency of discovering unique testcases. We implement prototype systems on multiple state-of-art fuzzers, and perform evaluations on two datasets. Our proposed method improves both the number of unique paths and unique bugs on real-world datasets. In addition, we discover 30 zero-day vulnerabilities in eight real-world programs, which demonstrate the effectiveness of FA-fuzz.

Sensitive resources in Trusted Execution Environment (TEE) have suffered serious security threats in recent years. Previous protection approaches either lack a strong assurance of TEE security properties or are limited to a single platform. We propose a compatible verified TEE architecture, calledCVTEE, which delegates a security monitor to manage TEE resources securely. This architecture has two key advantages: i) its functional correctness and security are guaranteed by a machine-checkable proof of security objectives of Trusted Application (TA) isolation, runtime confidentiality, and runtime integrity, and ii) it is applicable to different TEE platforms and implementation-independent due to its high level of abstraction and non-determinism of data types. Note that access control policy and information flow control policy are the core for security management of resources. After formally specifying the security attributes of TEE resources, we develop these policies based on Common Criteria (CC) in the security monitor and provide atomic interfaces.CVTEEis formally verified with 386 lemmas/theorems and$\sim$10,000 LOC of Isabelle/HOL. In addition, we implement a proof of concept for the access control module of Teaclave, and prove that the constructed access control model meets the security requirements through 5 theorems.

The challenge of requirements for the finer-grained isolated domain in Trusted Execution Environment (TEE) has been increasing, including the accuracy and security of resource management. However, the current access control mechanism for TEE cannot provide strict security assurances due to a lack of strict formal verification. In order to address the problem, in this paper, we first present the definition of multi-domain TEE, and propose a verified tag-based access control framework called REAL to provide the strict access control policy. We develop a high-level formal functional specification of REAL, and prove its correctness and security properties with 119 lemmas/theorems and ∼ 4,000 LOC of Isabelle/HOL. We also implement a page-level access control prototype called SOP-TEE and demonstrate that it correctly achieve the security objectives while merely incurring less than 0.3% overhead.

Summary Nowadays programmable logic controllers (PLCs) are suffering increasing cyberattacks. Attackers could reprogram PLCs to inject malware that would cause physical damages and economic losses. These PLC malwares are highly customized for the target which makes it difficult to extract a general pattern to detect them. In this article, we propose a PLC malware detection method based on model checking. Firstly, we improve the existing modeling method for PLC system by using the Satisfiability Modulo Theory (SMT) constraints to model the PLC system. We also present an algorithm that can transform the PLC program to the model. Our SMT‐based model can deal with the features of the PLC system such as undetermined input signals, edge detection and so on. Secondly, we focus on malware detection and propose two methods, invariant extraction and rule design pattern, to generate detection rules. The former can extract the invariants from an original program, and the latter can lower the bar for user to design detection rules. Finally, we implement a prototype and evaluate it on three representative ICS scenarios. The evaluation result shows that our proposed method can successfully detect the malwares using four attack patterns.

Physical unclonable functions (PUFs) are promising solutions for low-cost device authentication; hence, ignoring the security of PUFs is becoming increasingly difficult. Generally, strong PUFs are vulnerable to classical machine learning (ML) attacks; however, classical ML attacks do not perform well on strong PUFs with complex structures. Side-channel analysis (SCA) hybrid attacks provide efficient approaches to modeling XOR APUF. However, owing to the inadequate exploitation of all available data, recent SCA hybrid attacks may fail on novel PUF designs, such as MPUF and iPUF. Thus, herein, we introduce a method that combines challenge-response pairs with side-channel information to construct challenge-synthetic-feature pairs (CSPs) via feature cross, thereby making it possible to model strong PUFs through multiclass classification. We propose multiclass classification-based SCA hybrid attacks to model strong PUFs with complex structures. When provided with CSPs, the proposed hybrid attacks use a feed-forward neural network with a softmax activation function to build combined models of PUFs. The combined models predict class labels for given challenges and then reveal responses through simple mappings from these labels. Experimental results show that the proposed attacks could model 16-XOR APUF, (128,5)-MPUF, (8,8)-iPUF, and (2,16)-iPUF with accuracies exceeding 94%. Compared with state-of-the-art modeling techniques, the proposed attack has advantages in terms of modeling accuracy, time cost, and the size of required training data.

Summary ARM embedded devices are becoming increasingly ubiquitous, permeating many aspects of daily life. The security issues on ARM embedded devices are much more important in critical infrastructure. The trusted hardware technologies provide the trusted environments isolated from the untrusted part of the system. However, for some deficiency, the researchers focus on current hardware‐assisted isolated mechanisms. Depending on the implementation of the protection mechanism, the software‐based approaches are not efficient and the hardware‐based approaches are not flexible. Moreover, these defense mechanisms need formal specification that is inadequate in recent research. B method is a state‐based formal method, which provides a successive refinement mechanism. In this paper, we propose a hardware‐assisted memory isolation protection mechanism, provide specifications and refinements using the B method, and implement the memory management system on an ARM‐based platform. The evaluation results show that the proposed isolation protection mechanism is effective, and the automatic proof rate of machines is acceptable.

Summary This paper discusses security issues on the user equipment, which is the “last mile” of social networks. One of the main Achilles' heel of social networks is not the organization of networks themselves, but the user devices, typically Android ones. The existing system of privileges makes it easy to infiltrate the network via applications installed on users' devices. Conventional signature‐based and static analysis methods are vulnerable. Access to privacy‐ and security‐relevant parts of the application programming interface is controlled by the corresponding permission in a manifest file. While requesting access to permissions, it may offer opportunities to malicious codes, which will cause security issues. Few works among permission analysis, however, pay attention to the prevention of permission leakage on both hardware and software frameworks. In this paper we tackle the challenge of providing our multilayered permission‐based security extension scheme on Android platforms. We propose a usage and access control model and an effective method of preventing permission leakage based on ARM TrustZone security extension mechanism. In contrast to previous work, the proposed security architecture provides a permission‐based mandatory access control on Android middleware, Linux kernel, and hardware layers. The evaluation results demonstrate the effectiveness of the proposed scheme in mitigating permission leakage vulnerabilities.

The rapid development of information and network technologies motivates the emergence of various new computing paradigms, such as distributed computing, cloud computing, and edge computing. This also enables more and more network enterprises to provide multiple different services simultaneously. To ensure these services can only be accessed conveniently by authorized users, many password and smart card based authentication schemes for multiserver architecture have been proposed. Recently, Truong et al. introduced an identity based user authentication scheme on elliptic curve cryptography in multiserver environment and claimed that their scheme is secure against popular attacks. However, in this paper, we point out that their scheme suffers from offline password guessing and impersonation attack and fails to achieve security requirements of this kind of authentication scheme. Moreover, we put forward a new scheme to conquer security pitfalls in the above scheme. Security analysis indicates that the proposed scheme can be free from well-known attacks. Performance discussion demonstrates that our scheme has advantages in terms of both security property and computation efficiency and thus is more desirable for practical applications in multiserver environment.

Analysis of cryptographic algorithms is becoming more and more important in information security and malware analysis community. In this paper we have studied the static and dynamic characters of cryptography algorithms in program application by reversing a great lot of samples, and have summarized the static characters as crypto constants, lots of bit wise and arithmetic, logical expression, leaf functions and standard library by IDA. For dynamic characters, we have applied pin-tool to extract the characters as dynamic constants, dynamic statistic and memory operation data. Each static and dynamic character also has relevant sample to validate. Lastly, general comparisons have also been taken between these two kind characters and also have brought forward the future work.