Blockchain model checking

 Model Checking for Security of Supply Chain

Robert Wahlstedt

Dr. Mercer

Liberty University

CSCI 612-D02 LOU

November 4, 2019

 

2 / 3

I. Application of blockchain technologies in under equipped pharmacy supplies

a. Some countries such as Kenya has bad actors in the pharmacy supply line who seek to make money selling fraudulent products in their biomedical products which are cheaper to take advantage and make money ("Fake Drugs Are A Major Global Problem, WHO Reports", 2019).

b. Sometimes these actors put in chemicals which are actually known toxins such as floor wax ("Fake Drugs Are A Major Global Problem, WHO Reports", 2019).

c. In the United States pharmacies can detect fraudulent chemicals with equipment such as spectroscopy, pharmacies which are underfunded may not be able to afford such equipment.

d. Medtrace is a program which seeks to ensure the supply chain remains free of such actors by utilizing blockchain ("MedTrace - About", 2019).

e. What gives Blockchain its value is that it can be trustworthy.

f. Pslams 22:4-5 says “In You our fathers trusted; They trusted and You delivered them. To You they cried out and were delivered; In You they trusted and were not disappointed.”

II. Significance of efforts in work in blockchain development

a. Daniel 2:45 observes "In as much as you saw that a stone was cut out of the mountain without hands and that it crushed the iron, the bronze, the clay, the silver and the gold, the great God has made known to the king what will take place in the future; so the dream is true and its interpretation is trustworthy."

b. While great emphasis is placed on making harder problems to secure blocks from a blockchain, not enough emphasis is given to the accuracy of data streams given the real-time nature of these distributed systems.

c. It is possible using a framework such as AKKA to use futures, a data structure which is used to retrieve the result of some concurrent operation (Roestenburg, Bakker & Williams, 2016).

d. Functional programming languages which are pure languages discourages the use of mutable data types because they do not scale in parallel systems

e. Blockchain has a goal of multi-party non-repudiation which becomes more complicated as both the number of information providers and information consumers increase in number.

f. In March, 2013, Bitcoin found an error in the blockchain protocol when Bitcoin Core v0.8.0 failed to enforce lock limits and it lead to upgraded nodes splitting the network ("Block size limit controversy - Bitcoin Wiki", 2019).

g. “In each case, the objective of the attacker may be either to deduce the answer to a query he hasn’t already made (a forgery attack), or to recover the key (unsurprisingly known as the key recovery attack”) (Anderson, 2008).

III. Research on distributed database design can influence better blockchain implementation

a. Proverbs 12:17 “He who speaks truth tells what is right, But a false witness, deceit.”

3 / 3

b. Distributed computing is taking advantage of a network of computers so that the computers do not rely on each other and they share nothing (Dongarra et al, 2003).

c. “Mulitple users can access databases --- and use computer systems – simultaneously because of the concept of multiprogramming, which allows the computer to execute multiple programs – or processes at the same time” (Elmasri and Navathe, 2007).

d. Many IOT devices do not have resources but take part in blockchain.

IV. Cased based reasoning

a. Deuteronomy 25:13-16 says “You shall not have in your bag differing weights, a large and a small.  "You shall not have in your house differing measures, a large and a small.  You shall have a full and just weight; you shall have a full and just measure, that your days may be prolonged in the land which the LORD your God gives you. For everyone who does these things, everyone who acts unjustly is an abomination to the LORD your God.”

b. When attackers desire to take over a cryptographic system, they sometimes would want to issue command statements which are intentionally ambiguous to cause faults which could provide useful diagnostic data (Ahamad, 2016).

c. When Blockchain, a distributed system, experiences message loss, it cannot be guaranteed that it would arrive as intended to the receiver (Wattenhofer, 2016).

d. “Case-based reasoning suggests a model of reasoning that incorporates problem solving, understanding, and learning and integrates all with memory processes” (Kolodner, 1997).

e. With model checking it is possible to test concurrent systems for different properties including deadlock freedom and invariants that require proper request-response property handling (Gritzalis, Toone, Gertz & Devanbu, 2003).