Biblio

Bitcoin [1] as a popular digital currency has been a target of theft and other illegal activities. Key to the forensic investigation is to identify bitcoin addresses involved in bitcoin transfers. This paper presents a framework, FABT, for forensic analysis of bitcoin transactions by identifying suspicious bitcoin addresses. It formalizes the clues of a given case as transaction patterns defined over a comprehensive set of features. FABT converts the bitcoin transaction data into a formal model, called Bitcoin Transaction Net (BTN). The traverse of all bitcoin transactions in the order of their occurrences is captured by the firing sequence of all transitions in the BTN. We have applied FABT to identify suspicious addresses in the Mt.Gox case. A subgroup of the suspicious addresses has been found to share many characteristics about the received/transferred amount, number of transactions, and time intervals.

While the standard language XACML is very expressive for specifying fine-grained access control policies, defects can get into XACML policies for various reasons, such as misunderstanding of access control requirements, omissions, and coding errors. These defects may result in unauthorized accesses, escalation of privileges, and denial of service. Therefore, quality assurance of XACML policies for real-world information systems has become an important issue. To address this issue, this paper presents a family of coverage criteria for XACML policies, such as rule coverage, rule pair coverage, decision coverage, and Modified Condition/Decision Coverage (MC/DC). To demonstrate the assurance levels of these coverage criteria, we have developed methods for automatically generating tests, i.e., access requests, to satisfy the coverage criteria using a constraint solver. We have evaluated these methods through mutation analysis of various policies with different levels of complexity. The experiment results have shown that the rule coverage is far from adequate for revealing the majority of defects in XACML policies, and that both MC/DC and decision coverage tests have outperformed the existing methods for testing XACML policies. In particular, MC/DC tests achieve a very high level of quality assurance of XACML policies.

With the increasing inter-connection of operation technology to the IT network, the security threat to the Industrial Control System (ICS) is increasing daily. Therefore, it is critical to utilize formal verification technique such as model checking to mathematically prove the correctness of security and safety requirements in the controller logic before it is deployed on the field. However, model checking requires considerable effort for regular ICS users and control technician to verify properties. This paper, provides a simpler approach to the model checking of temperature process control system by first starting with the control module design without formal verification. Second, identifying possible vulnerabilities in such design. Third, verifying the safety and security properties with a formal method.