Interactive proof assistants such as Agda have powerful applications in proving the correctness of software. Non-terminating programs, such as those containing infinite loops, result in execution paths of infinite length, which can introduce challenges when reasoning about such programs. Agda, as a total language, relies on the concept of coinduction for reasoning about potentially infinite structures. Mutiple methods for coinduction exist in Agda, each with difficulties related to usage or soundness. To evaluate these limitations, I implement traces and semantics for a simple imperative programming language, While, using Agda's various methods of coinduction. The different encodings are compared in their abilities and limitations, and from this I identify areas for improvement in Agda's coinduction support. ... Read more

This thesis explores the formalization of Linear Temporal Logic (LTL) within the Agda proof assistant, focusing on the use of coinductive techniques to model infinite structures. Two primary questions guide this investigation: how can coinduction be employed to represent LTL formulas, and what are the limitations of Agda in doing so? To address these, the thesis presents two encodings of LTL: a deep embedding that models both syntax and semantics, and a shallow embedding that treats LTL propositions as infinite streams. Both approaches are evaluated by formalizing logical properties, deriving inference rules, and encoding the Towers of Hanoi as a temporal state system. The results demonstrate that coinductive techniques in Agda are expressive enough for reasoning about temporal logic, though challenges such as limited support for coinduction and usability issues remain. The findings provide insights into the strengths and limitations of Agda for modeling temporal logics and suggest directions for future work, including the exploration of sized types and extensions to first-order temporal logic. ... Read more

The proof assistant Agda supports coinduction, which can be used to reason about infinite and cyclic structures. The possibilities and limitations of using coinduction in Agda are not well known. To better understand these, I will implement Finite State Automata and their equivalence in Agda. Finite State Automata (FSA) is an example of a cyclic structure. FSA are an introductory model in computation theory, and can be used text processing and hardware design. Equivalence of two FSA is used in software and hardware verification. I created various encodings for FSA and prove equivalence between two deterministic FSA for each of them. At the end, I compared them and see whether they are limited by the support for coinduction in Agda. ... Read more

Coinduction is used to model infinite data or cycles in Agda. However, it is not as well explored in Agda as induction. Therefore, support for it might be lacking compared to induction. I explore how this applies for the evaluation of lambda calculus, what the different encodings of lambda calculus using coinduction are, and how they compare to each other and to an inductive evaluator. The two models I looked at are modelling cycles in variable references and modelling cycles in recursive variables. Cycles in variable references can be modelled coinductively, however, they do not help with evaluation. Since the evaluator is not coinductive, it is not accepted by the termination checker, therefore, it is not safer than an inductive evaluator. Encoding recursion using coinduction does make the evaluator terminate, aiding in creating a correct evaluator. This comes with the downside of sacrificing clarity and ease of reasoning about the code. ... Read more

Graphs are a widely used concept within computer science. Modelling graphs can be done in various ways, but the most popular approach is doing so inductively. When graphs contain cycles modelling them becomes less intuitive. A solution for this is using the dual of induction called coinduction, which has not been as well researched as induction. In this paper I explored the possibilities and limitations of coinduction in Agda by modelling graphs using coinduction. I looked at the struggles I encountered while coding in Agda. I also provide implementations of the graphs encodings. Suitability of the encodings is determined through experiments, in which properties about graphs are proven. Both guarded coinduction and musical coinduction were successful in all of the experiments. Creating an implementation using sized types was not successful. The main improvements I identified are concerning the ease of use for a new user of Agda. I recommend improving the documentation as well as the clarity of the error messages. ... Read more

Interpreted applications are often vulnerable to remote code execution attacks. To protect interpreted applications, we should reduce the tools available to the attackers. In this thesis, we investigate the possibilities for the automation of policy generation for interpreted applications in terms of system call arguments. These policies are used for system call argument interposition. We compare two approaches working on the interpreter to find if any of these two can provide meaningful policies. The first is dynamic analysis, and the second is static analysis, which uses symbolic execution.

The symbolic execution was least effective as it provides policies only for a small portion of the system call arguments, less than ten per cent, and hinders normal execution of applications with these policies. The dynamic analysis solution fares better, providing a restriction for about forty per cent of the system call arguments. We conclude that automatic policy generation of system call arguments for interpreted applications is a meaningful endeavour. ... Read more

As the world continues to embrace cloud computing, more applications are being scaled elastically. Elastic scaling allows applications to add or remove computing resources based on the load experienced by the application. When the load is high more resources are provisioned enabling the application to keep up with the load. When the load is low resources are removed ensuring that no resources are sitting idle. When implemented correctly elastic scaling allows applications to use fewer resources while maintaining application performance. One type of application that can benefit greatly from elastic scaling is a distributed stream processing application. Distributed stream processing applications are suited well for elastic scaling because the data coming through the data stream can be dynamic. This dynamic data stream makes it difficult to provision the right amount of computing power. One way to solve this problem is by using an auto-scaler that elastically scales the stream processing application. In this thesis, we compare different auto-scaling techniques for the distributed stream processing application Apache Flink. We implement a modern version of DS2 using metrics native to Apache Flink. An auto-scaler designed specifically for Apache Flink by Varga et al.. A modified version of the Dhalion, and a simple CPU based Kubernetes Horizontal Pod Auto-scaler (HPA). We compare the auto-scalers on the average number of resources used, the average latency, and the number of re-scale operations. Our results show the importance of a cooldown period between scaling events. The benefits of incorporating metrics from the message queue into the scaling decision, and that throughput based evaluation methods work well for determining by how much to scale.


... Read more

Users of anonymity networks face differential treatment and sometimes get blocked by websites, it is currently unclear how common this blocking is. This research aims to provide an overview of how common this blocking is while utilizing the AN.ON anonymity network. The analysis is accomplished by utilizing automated web scraping and processing to recognise and classify blocks by comparing them to a control connection. This process and software can be used and extended to analyze and compare any two connections. The scope is limited to the one thousand most popular websites according to the Alexa rating. Different kinds of blocks were identified and automatically recognised in processing, though manual verification is still required. Evidence is found and presented that there is a significant amount of blocking, occurring on approximately 23% of the analyzed domains. There is also a significant difference in blocking between using different cascades. ... Read more

Anonymity networks, such as The Invisible Internet Project, commonly known as I2P, enable privacy aware users to stay anonymous on the Internet and provide secure methods of communication, as well as multi-layered encryption. Despite the many innocent reasons users opt for online anonymity, these particular networks are censored at times, as they are associated with criminal activity. The goal of this paper is to measure to what extent I2P network users are being blocked by popular websites, and not, however, by governments or internet service providers. To establish this, we developed a web crawler which compares the responses to HTTP(S) GET requests sent anonymously, via I2P, and non-anonymously. Our results are based on the analysis of the received HTTP status codes, and on screenshots of the requested websites, to assess content blocking. This experiment shows that I2P users suffer from some form of blocking in 10.09% of cases. However, it should be noted that I2P faces certain bandwidth limitations and traffic congestion at the outproxy. This is a result of the fact that I2P was not designed with the intent of being a proxy to the Internet, but rather a self sustaining peer-to-peer network. ... Read more

Censorship and privacy issues have led people to use VPNs when accessing the internet. These VPNs not only try to protect their user but they are also associated with criminality and cyber attacks. Because of this, websites have started to resort to blacklisting the IP addresses that are used by the VPNs, thus blocking both genuine and malicious users. This forces users to sacrifice privacy for accessibility. This paper provides a method on how to measure the amount of blocking that VPN users experience and to be able to determine what type of blocking is occuring. This method is then used in an experiment using a web crawler where nodes from ProtonVPN are used to measure the amount of blocking that occurs while browsing the internet’s most popular websites. This experiment shows that on average 1.12% of the domains perform some type of blocking directed towards the VPN user and that the majority of this blocking consists of a total block, which means that the user is entirely excluded from any use of the website. Next to this it is shown that not all VPN nodes show the same amount of blocking and that there was no large difference in blocking found between days while using the same VPN node. It also shows that the categories which perform the most blocking are Business, Online Shopping and News. ... Read more

The LND is currently the most popular routing algorithm used in the Lightning Network, the second layer solution to Bitcoin’s scalability. Despite its popularity, recent studies demonstrate that its deterministic nature compromises the anonymity of the Lightning Network. In other words, threatening parties present in the transaction path can guess the sending and receiving parties of transactions easier than in the absence of such strong determinism. As a solution, we propose augmenting the LND with a length bounded random walk insertion to include randomness into the transaction path and regain anonymity. Most importantly, we found that for generated network simulations and the snapshot network, including the random walk into the transaction path improves anonymity. In simulations with LND routing, attackers could identify senders or
receivers for 70% of transactions. For simulations of networks with 100 nodes and an average of 2 edges per node with the weighted random walk insertion, attackers could identify senders or receivers around 65% of the time. However, for simulations of networks with 500 nodes and an average of 10 edges per node with the weighted random walk insertion, attackers could never identify senders or receivers. Besides, for the snapshot simulation, they could only identify either in around 4% of transactions. Thus, we overall believe that the random walk insertion into the LND algorithm addresses the anonymity issue of the unmodified algorithm. ... Read more

The Lightning Network is a second layer payment protocol built on top of Bitcoin, which is scalable and has reduced transaction fees. It does so by eliminating the need to broadcast every transaction to the whole network. When one user wants to send a payment to another, the routing protocol generates a path between them that is always fast and cost efficient. The low degree of randomness in the existing routing protocols during path selection allows an adversary to compromise the anonymity of the sender and recipient.
In this work, we propose a new routing algorithm that is less predictable when creating a transaction path. We show that this increases the anonymity of the users of the Lightning Network by creating an attack on the new routing protocol. The attacker tries to identify the potential source and recipient of a transaction. Our results suggest that there is a trade-off between the offered anonymity and transaction fees; it is not possible to get higher anonymity at no cost by designing a non-deterministic routing algorithm. ... Read more

The Bitcoin Lightning Network is a layer-two solution that promises instant payments, scalability, and low transaction fees on top of the Bitcoin blockchain. In case there is no direct channel between the sender and receiver, the routing algorithm uses source routing and a shortest path algorithm to determine the hops in a transaction. However, the lack of randomness in the routing decision allows an attacker to de-anonymize either sender or receiver, if they happen to be one of the nodes in the transmission path. The guarantees offered by the onion routing style algorithm are not enough to ensure anonymity when little to no randomness is used when choosing the path. Here we show how it is possible to modify the path finding algorithm keeping backward compatibility. It increases anonymity between the sender and receiver adding random hops to the already computed shortest path. Anonymity and efficiency metrics are then analysed with respect to an adversary that is aware of the full protocol implementation. Furthermore, assuming a protocol-aware adversary, an attack is designed, and it is concluded to be successful at most 53\% of the time and singularly de-anonymizing both parties in 1\% of the cases. The average number of hop counts increases by approximately two and the average fee paid by the sender increases by 4.77 times. Our results suggest a possible increase in the anonymity offered without a significant impact on the complexity of the lightning protocol implementation. However, transaction fees and payment success ratio should be analyzed further, especially for low-value transactions. ... Read more

Tor is the most popular tool for anonymous online communication. However, the performance of Tor's volunteer-run network is suboptimal when network congestion occurs. Within Tor, many connections are multiplexed over a single TCP connection between relays, which causes a head-of-line blocking problem, degrading relay performance. In this thesis, Tor's TCP transport layer protocol is replaced by QUIC, a UDP-based protocol that natively supports multiplexing streams asynchronously, effectively solving head-of-line blocking. Its performance is evaluated within various network environments through Containernet, a flexible Docker-based network test bed that allows for simple reproduction of results. Along with testing multiple congestion control algorithms, the impact of using Hystart++ within Tor over QUIC is evaluated. It is found that QUIC over Tor can perform up to 50% better in time to last byte performance than vanilla Tor in a realistic network environment, while featuring more consistent time to first byte performance. Additionally, the evaluations shows that throughput consistency and fairness amongst downloaders are improved as well, Besides offering improved performance, Tor over QUIC is designed with deployability and security in mind. This makes QUIC an attractive replacement as Tor's transport layer protol. ... Read more