From 7c04871fb32d58773b29d25cb33906247e79c81c Mon Sep 17 00:00:00 2001 From: POTHURI HARIKA <cb.en.p2cys21018@cb.students.amrita.edu> Date: Fri, 27 Jan 2023 11:11:31 +0530 Subject: [PATCH] Added introduction --- Introduction.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 Introduction.md diff --git a/Introduction.md b/Introduction.md new file mode 100644 index 0000000..712fda3 --- /dev/null +++ b/Introduction.md @@ -0,0 +1,16 @@ +### Smart Contract +A Smart contract is a self-executing code (agreement)between two or more parties deployed and executed in a distributed ledger platform. +### Formal Verification +Static analysis and a maths-based technique are called formal methods to check the system design and its properties. And it contributes to the safety and steadiness of the system as well as the functional correctness of the smart contract. +### Symbolic execution +All paths exploration.The execution makes use of “symbols” as inputs to the program and the results are expressed in terms of the symbolic inputs. +### Bytecode +Bytecode is written in low-level language that executes in environment like Ethereum Virtual Machine (EVM)). +### Model Checking +Model checking is a method for automatically verifying a system model with finite states against its specification. When it is used in smart contracts, model checkers perform verification of contract-level models, mainly transition systems, against a temporal logic specification. +### Runtime Verification and Testing +Runtime verification is a lightweight verification technique that checks the properties of a running program. In the domain of smart contracts, the term trace often denotes a sequence of instructions executed by a blockchain platform, while it can also refer to a sequence of function invocations or events emitted by a smart contract. Runtime verification usually provides a reactive defense against vulnerabilities or violations of correctness at runtime and can potentially identify vulnerable states that could not be reached by model checking or symbolic execution, due to the state or path explosion. +### Theorem Proving +Verification based on theorem proving involves encoding a system and its desired properties into a particular mathematical logic. +### Fuzzing +Fuzzing is a technique for finding software bugs by inputting a large number of randomized test cases to a program. The goal is to discover unexpected or undefined behavior, such as crashes or memory leaks, that may indicate a vulnerability. Fuzzing can be automated using specialized tools, and is often used in security testing and software development. It can be used to test a wide range of software, including operating systems, file formats, and network protocols. -- GitLab