| 1. |
- Gissurarson, Matthías Páll, 1991, et al.
(författare)
-
Short Paper: Weak Runtime-Irrelevant Typing for Security
- 2020
-
Ingår i: PLAS 2020 - Proceedings of the 15th Workshop on Programming Languages and Analysis for Security. - New York, NY, USA : ACM. ; , s. 13-17
-
Konferensbidrag (refereegranskat)abstract
- Types indexed with extra type-level information are a powerful tool for statically enforcing domain-specific security properties. In many cases, this extra information is runtime-irrelevant, and so it can be completely erased at compile-time without degrading the performance of the compiled code. In practice, however, the added bureaucracy often disrupts the development process, as programmers must completely adhere to new complex constraints in order to even compile their code. In this work we present WRIT, a plugin for the GHC Haskell compiler that relaxes the type checking process in the presence of runtime-irrelevant constraints. In particular, WRIT can automatically coerce between runtime equivalent types, allowing users to run programs even in the presence of some classes of type errors. This allows us to gradually secure our code while still being able to compile at each step, separating security concerns from functional correctness. Moreover, we present a novel way to specify which types should be considered equivalent for the purpose of allowing the program to run, how ambiguity at the type level should be resolved and which constraints can be safely ignored and turned into warnings.
|
|
| 2. |
- Grieco, Gustavo, et al.
(författare)
-
QuickFuzz testing for fun and profit
- 2017
-
Ingår i: Journal of Systems and Software. - : Elsevier BV. - 0164-1212. ; 134:December 2017, s. 340-354
-
Tidskriftsartikel (refereegranskat)abstract
- Fuzzing is a popular technique to find flaws in programs using invalid or erroneous inputs but not without its drawbacks. At one hand, mutational fuzzers require a set of valid inputs as a starting point, in which modifications are then introduced. On the other hand, generational fuzzing allows to synthesize somehow valid inputs according to a specification. Unfortunately, this requires to have a deep knowledge of the file formats under test to write specifications of them to guide the test case generation process. In this paper we introduce an extended and improved version of QuickFuzz, a tool written in Haskell designed for testing unexpected inputs of common file formats on third-party software, taking advantage of off-the-self well known fuzzers. Unlike other generational fuzzers, QuickFuzz does not require to write specifications for the file formats in question since it relies on existing file-format-handling libraries available on the Haskell code repository. It supports almost 40 different complex file-types including images, documents, source code and digital certificates. In particular, we found QuickFuzz useful enough to discover many previously unknown vulnerabilities on real-world implementations of web browsers and image processing libraries among others.
|
|
| 3. |
- Mista, Claudio Agustin, 1991
(författare)
-
Automated Derivation of Random Generators for Algebraic Data Types
- 2020
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Many testing techniques such as generational fuzzing or random property-based testing require the existence of some sort of random generation process for the values used as test inputs. Implementing such generators is usually a task left to end-users, who do their best to come up with somewhat sensible implementations after several iterations of trial and error. This necessary effort is of no surprise, implementing good random data generators is a hard task. It requires deep knowledge about both the domain of the data being generated, as well as the behavior of the stochastic process generating such data. In addition, when the data we want to generate has a large number of possible variations, this process is not only intricate, but also very cumbersome. To mitigate this issues, this thesis explores different ideas for automatically deriving random generators based on existing static information. In this light, we design and implement different derivation algorithms in Haskell for obtaining random generators of values encoded using Algebraic Data Types (ADTs). Although there exists other tools designed directly or indirectly for this very purpose, they are not without disadvantages. In particular, we aim to tackle the lack of flexibility and static guarantees in the distribution induced by derived generators. We show how automatically derived generators for ADTs can be framed using a simple yet powerful stochastic model. This models can be used to obtain analytical guarantees about the distribution of values produced by the derived generators. This, in consequence, can be used to optimize the stochastic generation parameters of the derived generators towards target distributions set by the user, providing more flexible derivation mechanisms.
|
|
| 4. |
- Mista, Claudio Agustin, 1991, et al.
(författare)
-
BinderAnn: Automated Reification of Source Annotations for Monadic EDSLs
- 2020
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783030577605 ; 12222 LNCS, s. 25-46
-
Konferensbidrag (refereegranskat)abstract
- Embedded Domain-Specific Languages (EDSLs) are an alternative to quickly implement specialized languages without the need to write compilers or interpreters from scratch. In this territory, Haskell is a prime choice as the host language. EDSLs in Haskell, however, are often incapable of reifying useful static information from the source code, namely variable binding names and source locations. Not having access to variable names directly affects EDSLs designed to generate low-level code, where the variables names in the generated code do not match those found in the source code—thus broadening the semantic gap among source and target code. Similarly, many existing EDSLs produce poor error messages due to the lack of knowledge of source locations where errors are generated. In this work, we propose a simple technique for enhancing monadic EDSLs expressed using do notation. This technique employs source-to-source plugins, a relatively new feature of GHC, to annotate every do statement of our EDSLs with relevant information extracted from the source code at compile time. We show how these annotations can be incorporated into EDSL designs either directly inside values or as monadic effects. We provide BinderAnn, a GHC source plugin implementing our ideas, and evaluate it by enhancing existing real-world EDSLs with relatively minor modification efforts to contemplate the source-level static information related to variables names and source locations.
|
|
| 5. |
- Mista, Claudio Agustin, 1991, et al.
(författare)
-
Branching Processes for QuickCheck Generators
- 2018
-
Ingår i: Haskell 2018 - Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, co-located with ICFP 2018. - New York, NY, USA : ACM. ; 53:7, s. 1-13
-
Konferensbidrag (refereegranskat)abstract
- In QuickCheck (or, more generally, random testing), it is challenging to control random data generators' distributions---specially when it comes to user-defined algebraic data types (ADT). In this paper, we adapt results from an area of mathematics known as branching processes, and show how they help to analytically predict (at compile-time) the expected number of generated constructors, even in the presence of mutually recursive or composite ADTs. Using our probabilistic formulas, we design heuristics capable of automatically adjusting probabilities in order to synthesize generators which distributions are aligned with users' demands. We provide a Haskell implementation of our mechanism in a tool called DRaGeN and perform case studies with real-world applications. When generating random values, our synthesized QuickCheck generators show improvements in code coverage when compared with those automatically derived by state-of-the-art tools.
|
|
| 6. |
- Mista, Claudio Agustin, 1991, et al.
(författare)
-
Deriving Compositional Random Generators
- 2019
-
Ingår i: ACM International Conference Proceeding Series. - New York, NY, USA : ACM. - 9781450375627 ; 25 September 2019
-
Konferensbidrag (refereegranskat)abstract
- Generating good random values described by algebraic data types is often quite intricate. State-of-the-art tools for synthesizing random generators serve the valuable purpose of helping with this task, while providing different levels of invariants imposed over the generated values. However, they are often not built for composability nor extensibility, a useful feature when the shape of our random data needs to be adapted while testing different properties or sub-systems. In this work, we develop an extensible framework for deriving compositional generators, which can be easily combined in different ways in order to fit developers’ demands using a simple type level description language. Our framework relies on familiar ideas from the à la Carte technique for writing composable interpreters in Haskell. In particular, we adapt this technique with the machinery required in the scope of random generation, showing how concepts like generation frequency or terminal constructions can also be expressed in the same type-level fashion. We provide an implementation of our ideas, and evaluate its performance using real world examples.
|
|
| 7. |
- Mista, Claudio Agustin, 1991, et al.
(författare)
-
Generating Random Structurally Rich Algebraic Data Type Values
- 2019
-
Ingår i: Proceedings - 2019 IEEE/ACM 14th International Workshop on Automation of Software Test, AST 2019. ; , s. 48-54
-
Konferensbidrag (refereegranskat)abstract
- Automatic generation of random values described by algebraic data types (ADTs) is often a hard task. State-of-the-art random testing tools can automatically synthesize random data generators based on ADTs definitions. In that manner, generated values comply with the structure described by ADTs, something that proves useful when testing software which expects complex inputs. However, it sometimes becomes necessary to generate structural richer ADTs values in order to test deeper software layers. In this work we propose to leverage static information found in the codebase as a manner to improve the generation process. Namely, our generators are capable of considering how programs branch on input data as well as how ADTs values are built via interfaces. We implement a tool, responsible for synthesizing generators for ADTs values while providing compiletime guarantees about their distributions. Using compile-time predictions, we provide a heuristic that tries to adjust the distribution of generators to what developers might want. We report on preliminary experiments where our approach shows encouraging results.
|
|
| 8. |
- Mista, Claudio Agustin, 1991
(författare)
-
Language-Based Techniques and Stochastic Models for Automated Testing
- 2023
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- As software systems become bigger and scarier, automating their testing is crucial to ensure that our confidence in them can keep up with their growth. In this setting, Generational Fuzzing and Random Property-Based Testing are two sides of the same testing technique that can help us find bugs effectively without having to spend countless hours writing unit tests by hand. They both rely on generating large amounts of random (possibly broken) test cases to be used as inputs to the system. Test cases that trigger issues such as crashes, memory leaks, or failed assertions are reported back to the developer for further investigation. Despite being fairly automatable, the Achilles heel of this technique lies in the quality of the randomly generated test cases, often requiring substantial manual work to tune the random generation process when the system under test expects inputs satisfying complex invariants. This thesis tackles this problem from the Programming Languages perspective, taking advantage of the richness of functional, statically-typed languages like Haskell to develop automated techniques for generating good-quality random test cases, as well as for automatically tuning the testing process in our favor. To this purpose, we rely on well-established ideas such as coverage-guided fuzzing, meta-programming, type-level programming, as well as novel interpretations of centuries-old statistical tools designed to study the evolution of populations such as branching processes. All these ideas are empirically validated using an extensive array of case studies and supported by a substantial number of real-world bugs discovered along the way.
|
|
| 9. |
- Mista, Claudio Agustin, 1991
(författare)
-
MUTAGEN: Faster Mutation-Based Random Testing
- 2021
-
Ingår i: Proceedings - International Conference on Software Engineering. - 0270-5257. ; May 2021, s. 120-122
-
Konferensbidrag (refereegranskat)abstract
- We present MUTAGEN, a fully automated mutation-oriented framework for property-based testing. Our tool usesnovel heuristics to improve the performance of the testing loop, and it is capable of finding complex bugs within seconds. We evaluate MUTAGEN by generating random WebAssembly programs that we use to find bugs in a faulty validator.
|
|
| 10. |
- Mista, Claudio Agustin, 1991, et al.
(författare)
-
MUTAGEN: Reliable Coverage-Guided, Property-Based Testing using Exhaustive Mutations
- 2023
-
Ingår i: Proceedings - 2023 IEEE 16th International Conference on Software Testing, Verification and Validation, ICST 2023. ; , s. 176-187
-
Konferensbidrag (refereegranskat)abstract
- Automatically-synthesized random data generators are an appealing option when using property-based testing. There exists a variety of techniques that extract static information from the codebase to produce random test cases. Unfortunately, such techniques cannot enforce the complex invariants often needed to test properties with sparse preconditions.Coverage-guided, property-based testing (CGPT) tackles this limitation by enhancing synthesized generators with structure-preserving mutations guided by execution traces. Albeit effective, CGPT relies largely on randomness and exhibits poor scheduling, which can prevent bugs from being found.We present MUTAGEN, a CGPT framework that tackles such limitations by generating mutants exhaustively. Our tool incorporates heuristics that help to minimize scalability issues as well as cover the search space in a principled manner. Our evaluation shows that MUTAGEN not only outperforms existing CGPT tools but also finds previously unknown bugs in real-world software.
|
|
