Video annotation is a critical and time-consuming task in computer vision research and applications. This paper presents a novel annotation pipeline that uses pre-extracted features and dimensionality reduction to accelerate the temporal video annotation process. Our approach uses Hierarchical Stochastic Neighbor Embedding (HSNE) to create a multi-scale representation of video features, allowing annotators to efficiently explore and label large video datasets. We demonstrate significant improvements in annotation effort compared to traditional linear methods, achieving more than a 10x reduction in clicks required for annotating over 12 hours of video. Our experiments on multiple datasets show the effectiveness and robustness of our pipeline across various scenarios. Moreover, we investigate the optimal configuration of HSNE parameters for different datasets. Our work provides a promising direction for scaling up video annotation efforts in the era of video understanding.

Dysarthria is a speech disorder that limits an individual’s ability to clearly articulate, due to the weakening of the muscles involved in speech. Despite recent advances in Automatic Speech Recognition (ASR), the recognition of dysarthric speech remains a significant challenge because of the limited availability of dysarthric speech data, significant speaker variability, and the mismatch between typical and dysarthric speech patterns. This paper addresses these challenges by using transfer learning and Low-Rank Adaptation (LoRA) techniques to enhance the performance of the state- of-the-art ASR model Whisper on dysarthric speech. By fine-tuning Whisper with the TORGO dataset, this study aims to adapt the pre-trained models to better recognise dysarthric speech patterns, thus reducing Word Error Rates (WER) and improving accessibility for individuals with speech impairments. Experimental results indicate that this approach can improve speech recognition performance since the Large- V2, Large-V3 and the corresponding distilled models achieved a reduction in WER after fine-tuning. The Large-V3 model achieved the greatest relative WER reduction of 22.65%.

Dysarthria is a speech disorder commonly caused by neurological disorders such as strokes, cerebral palsy and Amyotrophic Lateral Sclerosis (ALS). The severity level of dysarthria greatly influences the appropriate treatment for a patient. However, assessing the severity of dysarthria in a patient is a time-consuming process that requires a trained speech therapist. Therefore the following work explores a variety of classifier architectures for automatic dysarthria severity assessment using Whisper encodings. The datasets used were MSDM and TORGO while the classifier architectures implemented included a Convolutional Neural Networks and Recurrent Neural Network variants. Across both datasets, the Gated Recurrent Unit network (GRU) achieved the best performance with 97.21% accuracy on MSDM and 97.47% on TORGO.

Automatic Speech Recognition (ASR) systems have transformed human-machine interaction, yet they often struggle with child speech due to the unique vocal characteristics. This thesis investigates age and gender biases, focusing on enhancing the performance of state-of-the-art ASR model Whisper on child speech. Initial experiments reveal significant disparities in recognition accuracy across age groups and genders within child speech, highlighting the critical need for targeted improvements. The study uses Low-Rank Adaptation (LoRA) to finetune the model using four child-specific datasets, aiming to simultaneously enhance recognition performance and mitigate biases. Results demonstrate substantial reductions in Word Error Rates (WER) and biases after finetuning, showcasing the effectiveness of transfer learning in addressing demographic inequality. Gender biases decreased by 32.77% relative to their initial values, and age biases also improved, with a relative decrease of 27.52% after finetuning. This research showcases the potential of tailored approaches to advance ASR technology for low-resource user demographics, with implications for improving educational and assistive technologies.

Index Terms: Automatic Speech Recognition, Child speech, Whisper ASR model, Age and gender biases, Low-Rank Adaptation, Transfer learning, Demographic disparities

As programming languages become ever more sophisticated, there is growing interest in powerful and expressive type systems. Substructural type systems increase expressiveness by allowing the programmer to reason about the number of times and the order in which variables can be used. This can be used to model different kinds of memory allocation and to construct more expressive interfaces. However, implementing complex type systems requires complex type checkers – this complexity increases the chances of bugs in the type checker itself, which could lead to invalid programs being accepted or valid programs being rejected. The consequences of such bugs can range from programmer frustration to critical errors in production systems.

In this thesis, we develop a correct-by-construction type checker for a toy language with a substructural type system. We use Agda’s dependent type system to intrinsically ensure the soundness and completeness of the type checker. We discuss the advantages and disadvantages of the correct-by-construction approach and find that its complexity likely restricts it to specific use cases.

Type-checkers are used to verify certain attributes of programs are correct. Avoiding bugs in type-checkers is especially important when accepting faulty programs has serious real-world consequences. Correct-by-construction programming aims to prevent such bugs by embedding proofs of a program's correctness within the program itself. However, this approach introduces different challenges, such as added complexity. Whether the benefits of correct-by-construction type-checkers outweigh these challenges for more complex language features remains uncertain. This paper investigates correct-by-construction type-checking for a toy language with polymorphic algebraic data types and pattern matching. We do this by implementing a type-checker in the dependently typed language Agda. We show that this approach guarantees a type-checker that does not accept ill-typed terms. Furthermore, we reflect on the challenges of this approach and argue that this approach should be used when a guarantee of correctness is required.

Typecheckers help avoid bugs in code by catching errors early. Their implementation can, however, be incorrect, leading to inconsistencies in their operation. This research explores how we can use Agda and correct-by-construction programming to create a typechecker guaranteed to be correct in its implementation. For this purpose, I based a toy language on the simply typed lambda calculus extended with records and subtyping. The resulting typechecker is proven to be sound and complete with respect to the typing and subtyping rules of the toy language. This paper compares the correct-by-construction method to existing typecheckers. The new approach offers a greater degree of trust in its implementation but comes at the cost of being more demanding to develop and maintain.

The Correct-by-Construction (CbC) programming paradigm has gained increasing attention, particularly with the rise of dependently typed languages. The CbC approach is often characterized as rigid, rule-based construction process making it suitable for critical infrastructure like type-checkers, which are prone to bugs as they become more complex. However, the specific advantages and disadvantages of using the CbC approach for developing type-checkers in comparison to traditional programming languages remain unclear. Therefore, we investigate the development of a type-checker for a toy programming language extended with checked exceptions using the dependently typed programming language Agda. The results show that the CbC approach, combined with dependently typed languages, is highly effective for the very precise task of type-checker development. Despite the steep learning curve associated with these languages, this method offers notable benefits in ensuring the correctness and reliability of type-checkers. We conclude that this approach is a viable strategy for similar projects in the future.

Static type systems ensure code correctness by aligning implementations with defined type signatures. Despite their benefits in preventing common errors, complex type systems increase the likelihood of bugs within type checkers. Correct-by-Construction (CbC) programming offers a solution by using precise types to create intrinsically verified type checkers, ensuring soundness and potentially completeness. This paper evaluates the use of CbC programming for implementing type inference for the simply typed λ-calculus, focusing on Hindley-Milner (HM) and bidirectional type inference. Implementations in Agda, a dependently typed language, reveal that while CbC programming can eliminate bugs, it introduces significant complexity. HM type inference proves challenging in terms of soundness and completeness, whereas bidirectional type inference is easier to implement but still complex to prove complete. The study highlights the trade-offs of CbC programming, suggesting it is more suited for research and in-depth understanding rather than pragmatic programming.

Payment channels allow parties to utilize the blockchain to send transactions for a cheaper fee. Previous work has analyzed to which degree a party can profit by facilitating the transaction process. The aim is to increase the usability of the network and to be rewarded for providing this service. However, previous work focuses on maximizing the reward of the individual player in isolation, a model that we aim to expand. That is why in this work we extend the action space to allow other parties to act and react, and observe the impact this has on the rewards of the player that would otherwise act in isolation.
Testing existing placement strategies by performing channel placement games, we can assess the difference in the reward that indicates the potential loss that competition may cause when operating in the Bitcoin Lightning Network.
Furthermore, we have developed a new strategy that is able to improve the performance in the multi-actor model.

Malware poses a serious security risk in today’s digital environment. The defense against malware mainly relies on proactive detection. However, antivirus products often fail to detect new malware when the signature is not yet available. In the event of a malware infection, the common remediation strategy is reinstalling the system. However, the user loses their personal data, and thus it is not an ideal solution.

The academic works on malware remediation focus on system replay and recovery-oriented computing, which relies on heavy monitoring and is not suitable for a normal user’s personal computer. The work from Paleari et al. [31] proposed a remediation methodology that can be used entirely after the infection. They run the malware sample in the sandbox to observe the behavior and generate a revert operation for each action that modifies the system state. However, the limitation of such an approach is unable to deal with the potentially different behaviors in the sandbox and on the real hosts.

In this work, we propose a system that can generate user-specific recovery procedures, without the need of any monitoring in advance. We extend the work from Paleari et al. [31] by combining information from the infected machine. We first extract the environment configuration from the infected computer and configure the same context to the sandbox virtual machine, in order to eliminate the environmental influence on the malware’s behavior. After getting the behavior from the sandbox, we combine forensic evidence to understand the exact actions that happened on the system and generate the user-specific recovery procedures.

We implement a prototype based on Windows 10 and CAPE sandbox and perform an evaluation on 894 malware samples. We are able to recover 51.3% of the changes made by malware, which doubles the recovery rate compared to directly matching the sandbox result. Additionally, our experiment result also demonstrates significantly different actual behavior from the user’s machine and sandbox result. Our system design maximizes the use of information displayed in the sandbox, but the unshown behavior still leads to the biggest limitation of behavior-based recovery.

Scope graphs provide a way to type-check real-world programming languages and their constructs. A previous implementation that type-checks the proof-of-concept language LM, a language with relative, unordered, and glob imports, does not halt. This thesis discusses a five-step approach for constructing and type-checking a scope graph of an LM program. Using manually scheduled queries and auxiliary algorithms, type-checking the majority of examples failing in previous literature succeeds. The introduction of breadth-first-traversal and multi-origin querying is discussed as new scope graph primitives to aid in the reusability of this thesis for type-checkers that require stratified resolution.

Substructural typing imposes additional constraints on variable usage during type checking and requires specialized approaches to ensure type soundness. In this study, we investigate the implementation of a type checker using scope graphs for languages with substructural type systems. Scope graphs, a data structure representing scoping, provide a foundation for defining type checking algorithms. Our research project extends an existing Haskell library, incorporating typing rules for non-substructural, linear, and affine type systems. Through careful examination and comparison of scope graph and calculus implementations, we evaluate their expressiveness, extensibility, and readability. While the scope graph implementation demonstrates promising results, passing all test cases, the calculus implementation encounters unification errors in a subset of the tests. We conclude that the scope graph implementation offers a solid foundation for substructural typing, with potential for easy extension and integration with other language features. However, further work is needed to develop a comprehensive test suite and address the challenges faced by the calculus implementation. By advancing these areas, we can enhance the effectiveness of substructural type checking and enable more reliable and secure programming practices in languages with substructural type systems.

In this paper, we explore scope graphs as a formal model for constructing type checkers for programming languages that support type classes. Type classes provide a powerful mechanism for ad hoc-polymorphism and code reuse. Nevertheless, the incorporation of type classes into type checkers poses challenges, as it necessitates the resolution of instances and the assurance of coherence amidst overlapping instances. Our approach facilitates the separation of concerns between type class resolution and type checking, promoting extensibility and maintainability of the type checker. We contribute with a formal definition of scope graphs for languages with type classes, accompanied by algorithms for type class resolution and type checking. To assess the correctness of this approach, we implement a prototype type checker, and conduct experiments on a collection of representative programs. The results demonstrate the effectiveness of this baseline approach.

This paper investigates the viability of using scope graphs to implement type checkers for programming languages, specifically for a Scala subset. The primary objective is to determine if scope graphs can offer a declarative and extensible approach to type checking. To achieve this, we used a phased Haskell library to implement such a type checker. The declarativity and feature extensibility of the approach were evaluated by means of comparation with Rouvoet et al.'s approach in mini-Statix. The results demonstrate that using scope graphs as a basis for type checking yields a modular and extensible solution compared to traditional methods. However, it is noted that this approach may sacrifice a certain degree of declarativity. These findings suggest that scope graphs are a promising tool for type checking, particularly in the context of name binding. Further research is recommended to explore the possibility of implementing similar type checkers for other programming languages. Additionally, the paper suggests incorporating additional features into the targeted Scala subset, thereby enhancing its extensibility.

This thesis is a research into developing a methodology and implementation of automated gray-box Broken Access Control Scanning (BACS) in web applications. Broken access controls take first place in the OWASP Top Ten Web Application Security Risks 2021. The need for this research comes from the observation that testing for broken access controls in web applications is labor-intensive, time-consuming, and error-prone. Therefore, security researchers require a modern methodology and toolset for exhaustively discovering access control vulnerabilities in web applications.

The posited hypothesis is that the contextual awareness required for access controls can be achieved by assuming that users are only authorized to perform actions accessible via the UI for that particular user. The methodology developed in this research consists of four phases: 1) A crawl phase where an application is crawled as multiple users. 2) A request selection phase, where potentially vulnerable requests are selected. 3) A request replay phase, where selected requests are replayed in the session context of another user. 4) A response comparison phase to identify whether an access control vulnerability has occurred. An implementation is provided and evaluated during web application penetration tests of DongIT. The results show that critical and structural access control issues can be identified when all four stages are completed. However, the intricacies of web applications often pose challenges for one or more of the four stages. From the results, it is concluded that the BACS methodology is a viable strategy and a valuable tool in the toolbelt of a security tester.