Day20 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 3 minutes

author: aman

Blog VIII - Part I - Day 20

Hey there, Sorry for time being away.

In the complete series the main focus was to get the undergrads of my college to a kind of "ROAD" that is not taken "usually". This was something out of the world of Competitive Coding and Machine Learning. Since the Internet is Changing, and Blockchains are the one who is the Lead Changer of this internet revolution. I guess, transformation would be the right word.

We have discussed about a lot of things, let's put them together.

In this micro-blog

  • Connecting the Dots
Connecting the Dots

So, we've talked about a lot of things in the series of the Blogs. However, I must say that I couldn't cover everything I knew in detail, but here I'll try to connect the dots for you.

Let me list the blogs with the topics they covered. (You are free to skip through the list, just come back if you want to grab a look at what has been already done.)

We talked about various sotware attacks, attacks on Blockchains, how terminologies(soundness, completeness) could mean so much, vulnerabilities, specs/invariants, bugs in few of the most trusted spaces. We also had 2 guest lectures in the series. Let me now end up with a complex case in case of Bitcoin.

The case leaves a possibility for an attacker to Partiotion the Bitcoin network into multiple parts, creating a possibility to fork bitcoin into 2 parallel chains. Let's see how it works:

BGP Highjacking attack on Bitcoin

The Bitcoin network is highly centralised, even after known to be a decentralised network. And even if the Blockchain is completely encrypted the routing of messages is still very much open. The routes are easily deductible to the adversaries.

See Here :

To explain it more, the complete Bitcoin network is spread to multiple ISPs (Internet Service Providers), which are again built up of multiple network clusters, called as Autonomous Systems(ASes). To communicate some messages between these ASes uses a protocol called the Border Gateway Protocol(BGP). This complete complete procedure is termed as Internet Routing.

~13 ASes host about 30% of the entire network, while 50 ASes host the 50% of the Bitcoin Network

Any attacker with accesss to the routing infra, can Highjack the BTC network. As a result of attacking mentality they can partition the BTC network in several parts. Probably bringing a major network towards their side.

Now they can add as many blocks in their side, and broadcast the chain in the network. By the general rule of Bitcoin network, "the longest chain is considered to be the final chain", the malicious one gets updated in the real etwork.

"hese attacks, commonly referred to as BGP hijacks, involve getting a router to falsely announce that it has a better route to some IP prefix."

"50% of Bitcoin mining power is hosted in only 39 prefixes (i.e., in 0.007% of all Internet prefixes). This allows an attacker to isolate ~50% of the mining power by hijacking only these 39 prefixes. Much larger BGP hijacks (involving orders of magnitude more IP prefixes) are routinely seen in the Internet today."

You see this is a big thing. The Internet Routing has a developing history of more than 35 years, and the BGPs are still considered to be stable. It is said that, Bitcoin has already gone through hundreds of BGP routing attacks, and the attacks are still not deductible.

So turning back and seeing the dots to be connected, we find,

  • a 100% secure system isn't possible
  • not a lot of people are aroung the security of these systems
  • the higher institutes are still hustling to create an environment of secure information exchange
  • developing techniques to check a system for its security is extremely difficult, and this is the place where actual computer science comes in
  • the attack surfaces are open in Hardware devices as well,
  • the Finance field is already being exploited for its vulnerabilities and application for the Blockchain tech

One thing to notice is that, even if the Blockchain tech fails, there will be a definite transformation in the internet we will be using tomorrow.

The security is everything. For a world running on Data, User's privacy, access to the systems comes in first.

So, that should be a lot of motivation I guess. I don't have any pre compiled list of the things, one can work on in the future, but BLOCKCHAIN + SECURITY, is surely the most citable area of work.

I'll try to cover more in details sometime. And yeap, I never read the Blogs twice, so pardon for the errors.

Shoot your questions and error reporting here

- Aman Pandey

Day19 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 4 minutes

author: aman

Blog VII - Part I - Day 19

So, towards an end of this series.

I was quite busy in some other blog so couldn't write this one quickly.

In this blog I'll take up a case of a Security tool used in Ethereum Smart Contract bug discovery, ECHIDNA. I'll try to unwrap a few things about how a security can be used to analyse a "script", that governs the business of an organistion over Blockchain network. I'll try to cover almost everything taught last time in these 2 upcoming micro-blogs.

Let's take a look what's coming up...

In this micro-blog

  • One thing you can't believe in...
  • Fuzzer
  • Echidna
  • the Trail
One thing you can't believe in...

You might be having this strong image of BLOCKCHAIN, that a fraudulent transaction in a Blockchain cannot be reversed. Well...what is I say, it is actually inaccurate.

One of the famous article in MIT Technology Review, by Mike Orcutt, titled as "Once hailed as unhackable, blockchains are now getting hacked", stated the following:

"Blockchains are particularly attractive to thieves because fraudulent transactions can’t be reversed as they can be in the traditional financial system."

The statement is actually inaccurate!

Ethereum classic is an example to it. Remember, I've told you people before about the famous DAO attack. The had a massive $50 million money heist. Well the attacker is still a mystery.

The funds stuck until July 14, 2016. See the article. The possibility of attack was due to a vulnerable smart contract, that governs the functioning of DAO.

This was the problem until the Ethereum Chain was forked, after a long debate among the community. The transaction was rewritten in the new chain and now there exists 2 ethereum chain. One, that we use now, and where the DAO attack never happened. The other one, Ethereum Classic, where the DAO attack happened.

This is a note published by Vitalik Buterin, the founder of Ethereum Blockchain.

Strange!! yeah...?

Lets try to know about something which is used as a help to "not" get into such troubles...


Prevention is better than cure! Since, every crucial thing from a developer side depends on how well the contracts are written. If the contract does not release any possibility of attack, any loopholes of information leakage, the contract is probably secure.

Just like normal computer programs, there exists this old and always alive Computer Science (we may call it fundamental though). Analysing the programs statically and in dynamic environments to detect the bugs that can be triggered or are automatically getting triggered.

There are several techniques to anlayse a program. Symbolic analysis, Dynamic Analysis, Model Checking, Fuzzing...

There had been a lot of Security Tools in development recently. Here is a sophisticated list of all, in the official listings of

I will talk a bit about the only fuzzer system available for Smart Contract Analysis, by an Argentanian company TrailofBits. The tool is known as ECHIDNA.

Bonus excerpt(link)


day19_01 **pretty logo! isn't it?

ECHIDNA, is a property-based fuzzer system available for generating malicious inputs and break the smart contracts. It means, we write a certain property(like the one a system should "always" follow, or should "never" follow), and the system runs it on a local virtual machine, which is inbuilt with the tool. The system starts fuzzing. i.e. inputting the contract with random inputs, to check where the system fails the written property. These inputs are determined by input generation techniques, which are certainly in "possible limits" tha EVM can handle, and are not that arbitrary.

The tool is written in HASKELL, which is a FUNCTIONAL PROGRAMMING LANGUAGES, which you probably have never heard about. This means the code is short and does a lot. To give a intuitive brief, the Functional programming language are actually concerned about "What the thing is?" rather than "How the thing works?". Most of the SAT/SMT solvers, that I have talked about before are built over functional programming languages.

How ECHIDNA works? from user's point of view You write a smart contract with certain invariants(the property you think should never change and the smart contract should always follow). Then you run that within the system.

the Trail

After discussing all this... you must have got a great idea about what is actually going out around the world.

The next blog will be a very special Connect the dots... thing. Will have no technical knowledge.

I will just cover the things I & the 2 guests Kaushik & Gaurav has compiled for you people.

Will finally unveil the "The Road Not TAKEN..."


Day18 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 5 minutes

Hey guys, in this Blog I will be discussing the Integration of Blockchain with IoT (Internet of Things).

So, let’s proceed with what IoT actually is.

What is Iot?

Internet of things is an environment of connected physical devices embedded in various systems and accessible on the Internet, thus rendering these devices to become autonomous and can be controlled through their digital representation. The whole idea behind IoT is based on the transfer of data between two physical devices connected over a network and thus based on these data they act, like simulating the temperature of a house as in the case of smart homes, saving your attendance in a database as in for RFID.

Some of the industries and technologies developed on IoT includes smart homes, automotive environment, Healthcare, smart cities, smart grids, smartwatches, banking sector, etc.

perks of iot:

If technology is being used in multiple industries, it is a bit obvious that it should have some edge over the rest. The benefits of IoT are:

  • Communication: As discussed, it enables Machine-to-Machine(M2M) communication over the network on which both of them are connected.
  • Automation with control: Devices are controlled over a centralized wireless infrastructure, thus enhancing automation. This brings out an efficient communication between the devices, leading to output at a greater speed.
  • Monitoring over Information: The amount of data we receive through these IoT devices is enormous and hence it can be used to monitor the efficiency of these devices as well as take the algorithmic decisions more effectively due to this huge dataset.
  • Saves Money: Optimum usage of energy and resources with proper surveillance helps in avoiding possible shutdowns (as in industries), damages or waste of resources.

Thus, the price paid for implementing these IoT devices is very minimal when compared to the benefits it provides.

problems in iot:

“With a great amount of data comes out a greater responsibility to process it safely”.

The IoT network is a centralized one and also contains a large number of devices and involves the application of a huge set of data points, which requires security. This not only expands the attack surface, and hence IoT security and IoT privacy are huge concerns.

A case of such an IoT attack that took place in 2016, in this Mirai (a Botnet) penetrated in the domain name service provider Dyn and performed a DDoS (Denial of Service Attack) for a huge period, as a result, a large number of websites were down. It was achieved as the attackers gained access to this centralized network through the poorly connected IoT devices.

With such a huge vulnerability, it becomes non-practical to implement IoT in industries, Healthcare, or Banking sector where data security and privacy is a major concern. Also, the network is centralized hence the manufacturer, who is the most probable administrator to this can gain access to data. Hacker just has to find one vulnerability to gain access to the network and he will be able to gain control over the entire network.

Blockchain to rescue!!

To extend the properties of decentralization and data encryption to IoT, Blockchain is a major technology

being looked up to. Blockchain can ensure the decentralization of the network thus greatly reducing the

chances of any attacks on the IoT devices on the network. Also, encryption can be achieved at multiple

data entry points. Some of the features that can be added to IoT with the use of Blockchain are:

  • Identity: using a common blockchain network every node can identify all the devices. Data provided to the system is immutable and holds a record of every change in it. Also, the authentication of each device becomes more secure.
  • Scalability: using a blockchain network the fault tolerance and the system scalability also improves.
  • Security: blockchain can be used to secure the data contained in the network as transactions. Here, the data transfer is treated as a transaction that follows the rules set by the Smart Contracts.
  • Autonomy: using Blockchain the interaction of devices is decentralized and hence there are no servers. This makes the deployment of smart autonomous hardware possible for the service.
  • Secure code deployment: the deployment of codes into the devices also becomes more secure with the use of Blockchain. Thus, the developer can be confident that the code running on the device is the one he wrote and not the one by some malicious attacker.

problems in the integration

It’s not very simple to merge the two mentioned technologies which were not designed to work with one another and hence almost all the features that we added above as the benefits have certain restrictions.

Blockchain was made to be operated with much accessible Internet along with a device supporting high computational power which is not a property of IoT devices. Some other problems faced while the integration of the two is:

  • Storage capacity: IoT devices produce a huge amount of data in a real-time application while the blockchains we want to implement perform only a few transactions per sec. Thus, Blockchains are not meant to store this huge amount of data.
  • Security: the security problems at different levels furthermore increase with additional complexity as a result of a large variety of devices. Blockchain ensures the immutability of the data in the chains but cannot detect if the data received is already corrupt due to some hardware failure, environment change, etc. Thus, the IoT devices to be used on the blockchain need to be checked properly to avoid any such probable cause to occur.
  • Anonymity and data privacy: IoT devices that are used in the Healthcare sector or Banking sector deal with many private details and it is important to establish trust for data privacy and anonymity. But the problem of data privacy in IoT devices is complicated than the private and public Blockchain network as it starts with the collection of data and goes up to application level. 

    Hence securing the device requires the integration of security cryptographic software’s which generally harm the resource limitations of devices and hence economic viability.
  • Smart Contracts: the killer application of blockchain technology presents many challenges to IoT technology as they do not fit in IoT applications easily. Validation of these Smart Contracts is compromised if the IoT is not stable. Also accessing multiple data sources can result in overloading these contracts.
  • Consensus: the limited resource in IoT devices makes the PoW consensus unsuitable, there are other proposed consensus mechanisms (PoS, PoU, etc) but these are still not mature enough for their implementation. The initiatives have been taken of implementing full nodes into IoT devices, mining is a big challenge in IoT due to these limitations.


The Hybrid approach, using only a part of the interactions and data takes place in the blockchain and the rest are directly shared between the IoT devices, has been used in fog computation and is being tested for application in other domains, so we can safely say that the possibilities are high. Hope things work out well between the two great technologies.

Day17 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 3 minutes

author: aman

Blog V - Part II - Day 17

Hey People, I have given a gist of how the EVM stores the smart contracts on its machine.

In this I will directly discuss some technical things about, how deep you can dive into using just the information told about in the previoud micro-blog. Will try to give a glimpse, rest you can think of autonomously.

Let's do it...

In this micro-blog

  • Ethereum Virtual Machine (EVM)
  • The two Properties of EVM
  • How the Smart Contracts are actually stored?
  • Some supplementaries
  • These trail of Digits have some meaning
  • How can the attackers mis-use it?
Some supplementaries

I would suggest to open up following things in other tabs, would help you people throughout:

These trail of Digits have some meaning

I will keep this explanation as vague as possible, as we have some people onboard who have excitement about the blockchain, despite their core interests and Fields.

You know right, EVM is a Stack based machine, as 2 + 2 is actually written as 2 2 +, postfix notation.

If you break this "strange series of digits", 608060405234801561001057600080fd5b5060016000819055506......

according to as shown in tab.

Day17 - "Why?" & "What in?" Security & Blockchain?

EVM is a stack-based machine and for actions to happend on this machine, these trails are converted into the OPCODES.

Each OPCODE has a size of 1 byte. EVM has a set of 140 OPCODES in total

000060PUSH1 0x80
000260PUSH1 0x40
000861PUSH2 0x0010

Now, you understand how this thing works in EVM Stack? It would be infeasible to explain here how does a stack work. You better watch a video here call stacks & a big blog series here

If you are wondering how can you find the contract with that data? Well...just try copying pasting the following BYTECODE, and decompile in the, you'll find the same contract as was written in the previoud micro-blog simpleContract.sol.

How can the attackers mis-use it?

The level of publicity, Blockchain provides, any user can directly use the address of the contract deployed, to instatiate a variable of that, contract and call its various function.

This is not small, this can let the potential attackers exploit the contract and cause big-attacks like, DAO-Reentrancy attack, or DDoS Gas attack, explained in the previous blogs.

As I have told, these work as the fill in the blanks, the vacant spaces within the Bytecode are initiated by 0 , which is then replaced by the hexadec code of the input.

This contract is again deployed to replace the existing one, changing the current state of the contract.

The Internal checks verifies whether you are the authorised one to make a certain check or not.

IG, This concept is heavily used in off-chains, as well.


Find deeper readings here

Day16 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 3 minutes

author: aman

Blog V - Part I - Day 16

Hey People, I have been a little busy for last few days. Plus it took me some time to find the correct stuff that should fir right in the series.

So now, after so many micro-blogs, it is possible that you must be wondering on How an attacker can even do this? For that I'll be giving you people an idea about what things are openly available to people, potentially an attacker, to be able to exploit the weaknesses of the blockchain governing codes.

We'll take up Smart Contracts in world's larget Decentralised Application(dAPP) platform. Ethereum works with the currency called ETHER(ETH).

I will give you a quick look into what all information is publicly available, and an idea about what all can be extracted from the information available.

Lets dive deep in...

In this micro-blog

  • Ethereum Virtual Machine (EVM)
  • The two Properties of EVM
  • How the Smart Contracts are actually stored?
Ethereum Virtual Machine (EVM)

Ethereum, is actually a large collection of machines spread across the world in decentralised fashion. And a Ledger containing the details of all the transactions is distributed across all the machines(called nodes).

Ethereum Virtual Machine or EVM, is a system used to refer to this computer.

The two properties of this EVM

1) EVM is Quasi-Turing

A turing complete machine is the one, which is able to solve any problem provided to it, despite the fact how long does it take.

EVM is quasi-Turing because, it is limited by a factor, COST. Any computation you make to it, it is limited by the gas price required to solve this problem.

2) EVM is Stack Based Machine

EVMs Data Structure is Stack Based.

for e.g. 2 + 2 can be given as 2 2 +

How the Smart Contracts are actually stored?

If still you think the contract(i.e. the governing document on the Ethereum Blockchain), is stored in the textual format, as the following one, then you are absolutely wrong.

To work on EVM, the Smart Contracts are to be converted into a specific format called, the bytecodes.

After compiling the Smart Contract into the bytecode using Solidity compiler(solc), it is exported to the EVM.

  • Contract Bytecode: is the bytecode of the complete smart contract. That is actually, what ends up staying on the EVM.

It is comprised of functions(), already initialised variables, and all that is predefined. Plus, Something that can be changed during running.

  • Runtime Bytecode: it is the same bytecode that can be changes during running.

It can be said that Contract Bytecode = (some bytecode) + (Runtime Bytecode)*

-> Now, when compiled the above smart contract will look like,

if we compile it using solc --bin simpleContract.sol, we get the Contract Bytecode

======= simpleContract.sol:SimpleStorage =======


608060405234801561001057600080fd5b5060016000819055506 0c6806100276000396000f3fe6080604052348015600f57600080 fd5b506004361060325760003560e01c806360fe47b1146037578 0636d4ce63c146062575b600080fd5b6060600480360360208110 15604b57600080fd5b81019080803590602001909291905050506 07e565b005b60686088565b604051808281526020019150506040 5180910390f35b8060008190555050565b6000805490509056fea 265627a7a723158200e135b4c7bcf7bde9dca1f257d97637d8137 b315e29248b5654ac7830dab9e8264736f6c63430005100032

and, if we compile it using solc --bin-runtime simpleContract.sol, we get the Runtime Bytecode

======= simpleContract.sol:SimpleStorage =======

Binary of the runtime part:

6080604052348015600f57600080fd5b506004361060325760 003560e01c806360fe47b11460375780636d4ce63c146062575b6 00080fd5b606060048036036020811015604b57600080fd5b8101 908080359060200190929190505050607e565b005b60686088565 b6040518082815260200191505060405180910390f35b80600081 90555050565b6000805490509056fea265627a7a723158200e135 b4c7bcf7bde9dca1f257d97637d8137b315e29248b5654ac7830d ab9e8264736f6c63430005100032

If you look very closely, you get to find that, the "Contract Bytecode" contains the "Runtime Bytecode"

608060405234801561001057600080fd5b5060016000819055506 0c6806100276000396000f3fe6080604052348015600f57600 080fd5b506004361060325760003560e01c806360fe47b1146037 5780636d4ce63c146062575b600080fd5b6060600480360360208 11015604b57600080fd5b81019080803590602001909291905050 50607e565b005b60686088565b604051808281526020019150506 0405180910390f35b8060008190555050565b6000805490509056 fea265627a7a723158200e135b4c7bcf7bde9dca1f257d97637d8 137b315e29248b5654ac7830dab9e8264736f6c63430005100032

Metaphorically, the smart contract remain in a way of Fill in the Blanks! The arguments inside the function(), are the blanks, which gets filled, and the state of the Blockchain is changes, or the query result is returned.

Please Note! This thing is publicly available.

-> Will directly, continue in next microblog....

Day15 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 2 minutes

author: aman

Blog IV - Part II - Day 15

Let us get some dirty hands on with some more Solidity code and exploit a few more Ethereum - Solidity bugs.

Here we'll discuss about the famous DAO attack, caused by the reentrancy bug.

Let us do it...

In this micro-blog

  • delegatecall (the proxy calls) (SWC-112) (Inclusion of Functionality from Untrusted Control Sphere)
  • DoS With Block Gas Limit (SWC - 128)
  • Integer Overflow (SWC - 101)
  • Reentrancy Bug(DAO attack) (Improper Enforcement of Behavioral Workflow) (SWC-107)
  • uncheckedSend() (SWC - 113)
  • tx.origin bug
  • Variable Shadowing (SWC-119)
3. Reentrancy Bug(DAO attack) (Improper Enforcement of Behavioral Workflow) (SWC-107)

You can find the related files in this gist.

There are two files. One is simpleDAO.sol which is a simple DAO(Decentralised Autonomous Organisation) contract, which is generally available publicily. Other one is reentrancy.sol which is particularly written by the attacker to exploit this bug.

It is termed as Improper Enforcement of Behavioral Workflow, as the attacker is able to make improper use of the conctract function, and play with the workflow of the contract.

Now, look at the 2 very crucial parts of both the contracts, one from each.

-> Attacking contract

function() public payable{

The variable DAO is the instantiation of the already deployed contract.

-> DAO Contract

function withdraw(uint amount) public{
    if (credit[msg.sender]>= amount) {

Now, just go with the flow.

You being the owner of the "attacking contract", will trigger some function to withdraw your money from the DAO Contract, the flow goes as follows:

call is sent to function withdraw() [DAO]


the function checks whether you have that amount, which comes to be true


amount is transferred to your contract using sender function


to accept the payment, "payable" function of your contract automatically gets called


The flow moves again to the "withdraw()" Notice!!! the amount is deducted after sending the amount your contract

"Notice the credit[msg.sender]-=amount; line."


The flow repeats.


This thing, drained off all the money from the DAO contract to the attacker contract.

"One of the major dangers of calling external contracts is that they can take over the control flow. In the reentrancy attack (a.k.a. recursive call attack), a malicious contract calls back into the calling contract before the first invocation of the function is finished. This may cause the different invocations of the function to interact in undesirable ways."

*Can you Imagine what the Solution was?

Well, I'll tell that in the next blog. laughing

You are surely gonna kill me for this.

Be honest!!! dont search it up

*will be dropping an "answer" box in the cev insta page @cevsvnit

Thank you.

Adding gist frames here

Reentrancy Bug(DAO attack) (Improper Enforcement of Behavioral Workflow) (SWC-107)

Day14 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 3 minutes

author: aman

Blog IV - Part I - Day 14

Let us get some dirty hands on Solidity, to exploit some very dangerous Ethereum - Solidity bugs.

2 Bugs/vulenrabilities in this very micro-blog. Covering bugs like, Denial of Service with Block Gas Limit, where the attacker exploits the bug by taking benefit from limited GAS available for each transaction, and unchecked_send() bug, which when made by mistake, could be a disaster to the host contract holder, and users.

Let us do it...

In this micro-blog

  • delegatecall (the proxy calls) (SWC-112) (Inclusion of Functionality from Untrusted Control Sphere)
  • DoS With Block Gas Limit (SWC - 128)
  • Integer Overflow (SWC - 101)
  • Reentrancy Bug(DAO attack) (Improper Enforcement of Behavioral Workflow) (SWC-107)
  • uncheckedSend() (SWC - 113)
  • tx.origin bug
  • Variable Shadowing (SWC-119)
1. dos_gas.sol() [check out the exploitation of the bug at this gist])(

DOS with Block Gas limit is A denial of service attack, where a host contract denies to perform its duties due to limited amount of gas provided for each transaction (about 3 million).

    for(uint i=0;i<500;i++) {

Here to make the contract to always true change the upper bound of i to some lesser value, say i<100. Increase the value to fail it at a certain point.

uncheckedSend() [check out the exploitation of the bug at this gist])()

Whenever a contract, say sender, transfers the ether to another contract,say receiver, the payable function of the receiver is triggered, and this can be misused. For eg. payable function of the receiver contains some computationally heavy instructions, it can cause transfer() to fail and send() function to return false. Thus if the send() is not checked, it may cause a bug called uncheckedSend.

Also, since send() doesn't propogate the exception, its harmful of the users to use it.

contract attacker{
    bool public flag=false;
    function change() public{
		if(!flag) 	flag=true;
		else    	flag=false;
	function() external payable {if(flag)	revert();}
contract Test{
	attacker a = new attacker();
	bool private flag0 = true;
	bool private status;
	function set0(int val) public returns (bool){
    		if (val % 10 == 0) {a.change();}
    		else flag0=false;
    function echidna_send() public payable returns(bool){
            return address(a).send(0);
	function() external payable{}

Here, echidna_send() will be the main function whose bool value will be checked by the tool.

  • payable functions : payable functions are necessary for the contract to accept the ether. Whenever a contract, say sender, transfers the ether to another contract,say receiver, the payable function of the receiver is triggered.

  • echidna_send() : contains address(this).transfer(msg.value); which is responsible for transferring ether to the Test contract. Which will then be transferred to the the instance of the contract attacker, a. Note: we are transferring 0 ethers to the contract address and then to the instance a. As address.send() doesn't revert state whenever the payment fails. So we try to return its bool value, which is then catched by echidna_send(), and thus by the tool. This is the value that the tool mainly checks for, and thus will be able to tell whether the contract payment through send was completed or not.

  • set0(int val) : random value is provided to set0(int val) as argument. Which then waits for the no. satisfy the condition if (val % 10 == 0). As soon as this value is catched, it triggeres change() function of the contract.

  • change() : This is responsible for flipping the flag value. So as soon as this function is triggered, flag=false changes to true, and now revert state in the payable will be activated. Now, the contract attacker, will be reverting each transaction made to it.

So this is how it works: [a is the instance if contract attacker] We first start running the contract with a.flag == false, and wait for a value in set(int val), to flip the flag of contract a to true, and thus activating the revert in payable. This will fail everytime the payment is made. And since, the send() doesn't revery any exception, it shall revert true of false. Which is catched by echidna_send(), and will be returned to the tool, to state that the payment could not be completed.

View this thread for more about address.send and address.transfer

I took it exactly from the exploitation repo I made earlier. Please email directly, in case of any doubts:


Adding gist frames here

DoS With Block Gas Limit (SWC - 128)

uncheckedSend() (SWC - 113)


Day13 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 3 minutes

author: aman

Blog III - Part III - Day 13

Understanding Hyperproperties and Blockchain together. And how this could be so big!

Let's get in....

In this micro-blog

  • Let us check this vaguely
  • 2-trace property
  • Hyperproperties
  • Safety and Liveness - Another 2 very Important terms
  • Blockchain & Hyperproperties
  • How this could be so big?
Safety and Liveness - Another 2 very Important terms

As already explained, Property is a set of traces(traces are the set of System states). So, intuitively the Properties are the set of all the traces, where the system can reach.

Now, there are two things to be well noted, there are certain states "where a system should never reach & certain states where a system should eventually reach.

Well these are termed as "Safety" and "Liveness" trace properties. Where: Safety: is the property that prescribes that a system should never reach some bad state , while Livenes: is the property that prescribes that a system shoudl "eventually" reach some "Good State".

Give some time understanding this stuff. These are 2 very important terms when thinking about System proofs.

Every trace property is an intersection of safety & liveness property.

Blockchain & Hyperproperties

A very straight explanation from Hyperpoperties paper[1], says

"If systems are modeled as sets of execution traces [35], then the extension of a system property is a set of sets of traces or, equivalently, a set of trace properties. We name this type of set a hyperproperty."

Thus these safety and liveness property are said as heypersafety & hyperliveness.

Every property of any system anywhere can be defined in terms of these hyperproperties...

Now you must remember there was a CIA triangle, that Hrishabh explained about in Winter School 2019, which stands for : (take an example of something stored inside a locker)

C -> Confidentialitycan't see what is inside the locker
I -> Integritycan't tamper what is inside the locker
A -> Availabilitycan't destroy the locker's availability

If you think very crucially, you'll find that only confidentiality and intergrity are the two properties concerned with the secure information flow.

The most invincible idea behind blockchain is the safety of data.

To ensure the flow of data never goes in wrong hands, which is described by the very term secure information flow.

Now considering application of hyperproperties in the Blockchain, let us take 2 traces of blockchain:

π1 & π2.

There are two ways hyperoperties to check here!

  1. Non-interference: if some commands are issued by the high-level users (say the general of the army, that should not reach to the ears of the soldier). These should be removable, without the low-level user noticing any changes.
  2. Observational Determinism: System should always appear deterministic to the trusted users, or in this case high level users.

Suppose, in the blockchain, there are two traces, π1 & π2.

Day13 - "Why?" & "What in?" Security & Blockchain?

This is clipped form Dr. Pramod's teaching. It explains about Observational Determinism, but not with Blockchain

The upper one is π1(set of states as viewed by high level) and lower one is π2(set of states as viewed by low level).

High-Level user is that user, who can make changes to the Blockchain. And Low-level are the ones, who can just look at the states and retrieve data.

Now, whenever some critical input is given by the high level user(like, a general take some decision), it should not be noticed by the low-levels(the soldiers).

So, in OBSERVATIONAL DETERMINISM, the states of blockchain observed by both the low level and high level user should be same. (Notice that obsT between the two traces,showing the observations being made.)

That is all, this has a very crucial implications in the field of Systems, and even larger when applied to Blockchain.

How this could be so big?

This is very big thing. Though introduced back in 2003(observational determinism) & 1982(non interference), these hyperproperties turns out to be very crucial checks in the security.

Just consider a statement:

"If the low level is able to see the change made by the high level, there is the safety issues with Confidentiality adn Intergrity of the data."

Hope you got a very intuitive feel about these stuff.

Hope you had a great read.

See y'all....

Day12 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 4 minutes

author: aman

Blog III - Part II - Day 12

In this blog, we’ll vaguely discuss the Hyperproperties and Information Flow thing.

As continued, this blog will contain the understandings from the Teachings of Dr Pramod, from SAT SMT Winter School 2018[1]. I will try to portray my understanding from his teachings and is working with him closely on Blockchain, I suppose it earned me a proper understanding.

Let us do this....

In this micro-blog

  • Let us check this vaguely
  • 2-trace property
  • Hyperproperties
  • How this could be so big?
Let us check it vaguely

We'll play a game, known as Distinguishability Game.

We pose a challenge game between attacker and a defender, where the attacker needs to exploit flow of information and the defender has to prevent it.

2 people:


Situation: There are two systems behind a wall, say system_0 and system_1, and the attacker just have the access to a function foo(x). He doesn't know, whenever he makes a call, to what system does this does the call go to.

The attacker is just like any other user, but who is trying to attack an arrangement behind a wall, popularly known as adversaries.

The defender is the arrangement behind the wall, which diverts the calls to different systems, which have following secret keys: "secret_b" , where b -> {0,1}. i.e. secret_0 or secret_1.

Game Initialisation

  • secret_0 := {0,1,2,3}
  • secret_1 := {4,5,6,7}
  • publicx := {10,11,12,13}
  • whenever a normal user makes a call, "only publicx is called, and thus the values inside it are returned"

Game Execution

  • there are a lot of calls to foo(x) made from across the world, and by the users with different access levels, i.e. admins & normal user
  • so the calls by a normal user are interspersed calls made by the admins


  • if attacker is able to identify which system in system_b the call is sent to, he wins, as this information should not be made available to the "normal user"

---> Now consider the following picture


The attacker will try to observe the value of "r", and specially "he will be looking for any unexpected values"

Considering this program, try to make following calls to the system(both normal user and admins included),

• priv_level = sup_user, foo(1), obs = ∅ • priv_level = user, foo(1), obs = 11 • priv_level = sup_user, foo(2), obs= ∅ ........ These calls will go on forever the attacker will

But, now if the program has been like the following, and we bagin with our game:


we start with the following calls, (notice the introduction of variable t)


  • priv_level = sup_user, foo(1), obs = ∅
  • priv_level = user, foo(4),
    • obs = 2 -> b = 0
    • obs = 6 -> b = 1

Woosh!!! Did you realise here attacker wins the game, by observing the value of r & t.

If the value returned to the attacker is 2 clearly the secret key b, chosen will be b = 0 and if the value returned to the attacker is 6 clearly the secret key b, chosen will be b = 1

The system just leaked the information.

AFAIK, during my study I encountered this incident had already been reported, where the highly confidential data was leaked due a misprinted "=", I may be wrong though. But, This is a very critical exploitation of Information Flow.

In the very next blog, I'll take a use case of blockchain, and try to determine for such observations for it.

Thanks y'all..

and yeah, Amid this Corona virus thing, be safe...

_ Team CEV

Day11 – “Why?” & “What in?” Security & Blockchain?

Reading Time: 2 minutes

author: aman

Blog III - Part I - Day 11

Hope the blogs are going pretty well.

In this very blog, divided into several micro-blogs, I'll be explaining about the Hyperproperties. This particular thing will take you to the most obvious level of understanding the computer systems. And in this particular micro-blog, I'll tell about hyperproperties, directly.

Most of the work will be taken from the teachings of my mentor Dr Pramod Subramanyan[1], IITK. He is Doctorate from UPenn and Post-Doctorate from UC, Berkeley, and one of the smartest individual I have ever met.

I will try to prepare everything from my understanding...

In this micro-blog

  • Let us check this vaguely
  • 2-trace property
  • Hyperproperties
  • How this could be so big?

This excerpt is from #Day08 blog, where I have tried to give a few intuitive explanations about Formal Methods and Verifications.

Day11 - "Why?" & "What in?" Security & Blockchain?

This explains about the states.

One more definition I want to speak about is traces, which are just the sequence of states.

e.g. for a system S the Trace(S) can be intuitively understood as,

t1 = S1 -> S2 -> S3....

where, Sn is the state of the system, at a certain point.

"A Trace Property is a set of Infinite states."

"A hyperproperty is a set of sets of infinite traces, or equivalently a set of trace properties."

{{S1, S2, S3, ...}, {S1, S2, S4, ...}, {S1, S4, S6, ...} ....}

The interpretation of a hyperproperty as a security policy is that the hyperproperty is the set of systems allowed by that policy. Each trace property in a hyperproperty is an allowed system, specifying exactly which executions must be possible for that system.

Trace properties are satisfied by traces, whereas hyperproperties are satisfied by sets of traces.

These hyperproperties are largely employed as a tool to measure Secure information flow, and many other security issues.

Actually I started in the exact order written in the above checkbox. But switched it to explaining the Hyperproperties first. Just try giving a thought over, "Hyperproperties and Blockchain"

See y'all on the next blog...

CEV - Handout