Overleaf submission to arXiV

After scouring through the entire web for close to 5 years and giving up out of sheer frustration every time, I was finally able to upload my TeX sources to arXiv (as of 17.01.2024). The solution was buried as a comment to one of the lesser upvoted answers in a less popular StackExchange thread. I hope Google will push this post high up so that it can help Overleaf (and minted) users.

Read More

Unfolding Fix

In pure lambda calculus (untyped or typed) the fix combinator is used to encode recursion. fix represents the least fixed point of a function f i.e the least defined x for which f x = x. An important concept is that a function need not have a least fixed point. But for those functions which do, the least fixed point is the base case for recursion. An intuition about the least fixed point is :

Read More

Understanding the Transactional Nature of Smart Contracts

In this post I attempt to summarize my understandings about the transactional nature of Smart contract execution. I conducted this study, while trying to understand the DAO exploit. The basis of the DAO exploit is a recursive(or rather reentrant) message call. One important point to note that an exception(during a message call or otherwise) in the Ethereum Virtual Machine , would imply reverting all changes to state and balance. Solidity has a documentation on cases where exceptions are thrown automatically. However in certain cases like send we need to manually raise an exception using throw. So, the attacker has to be careful not to hit any exceptions while attempting the reentrant call to avoid reverting. I also rectify certain mistaken assumptions, I made in my previous post.

Read More

The Smart Contract and Transactional Memory Analogy

In this post and the coming ones, I will be detailing about a particularly interesting analogy between Smart Contracts and Transactional memory. And how we can use one to verify and reason about the other. The majority of this work has been driven by a paper by Dr. Ilya Sergey and Dr. Aquinas Hobor on similar grounds. My attempt has been to try and extend the ideas from this paper, to mitigate the issues plaguing Smart contracts and their semantics as listed in another paper on Making Smart Contracts Smarter. Essentially this serves as a literature survey as well as a playground for me to pitch my ideas unifying the 2 papers. Sounds interesting? Then read ahead. :)

Read More