[ { "title": "Type checker prototype for dynamic languages", "url": "https://mlaurent.ovh/projects/type-checker-prototype/", "body": "A type checker prototype for a custom functional language, featuring:\n\nSet-theoretic types (with intersection, union, negation and recursive types)\nPrecise types for functions, pairs and records\nParametric polymorphism\nType inference\nOptional user type annotations\nPrecise typing of type-cases (occurence typing)\nPattern matching\n\nSome missing features (and thus, future work):\n\nSupport of side-effects\nRow polymorphism for records\n\nThis prototype is implemented in OCaml (source code), and a (slow) web version using js_of_ocaml is available for testing.\nA DOI for an older version is available: http://dx.doi.org/10.1145/3462306\n" } , { "title": "Glitch: Arbitrary Code Execution for some Pokemon games", "url": "https://mlaurent.ovh/projects/ace-generator/", "body": "I think the game I played the most when I was a kid was Pokemon Ruby, on GBA.\nWith my brother, we completed the regional Pokedex, with 200/200 Pokemon catched.\nUnfortunately, there still were two Mythical Pokemons that we were unable to catch,\nand for a good reason: those were accessible only for those attending some physical events,\noccuring only in some places and sometimes only in Japan. This was the early time of forums,\nand lot of rumors started to flourish: you can unlock Deoxys by beating the Battle Tower,\nby waiting for the white stone of the spatial center to be stolen, etc...\nBut rumors, that's all they were.\nIn 2021, I got interested into the glitching scene, that is, how to exploit bugs and flaws in games\nin order to achieve things unplanned by the developpers. That's where I discovered that this wasn't a lie:\nit is indeed possible to catch Deoxys without attending physical events nor using any cheating device!\nThere are several methods to achieve it, but the most reliable and powerful way is via Arbitrary Code Execution (ACE).\nIt is the Holy-Grail of glitchers: exploiting the game until we are able to make it execute any codd we want!\nIf I find some time, I'll write some articles about it, because the process to get there is very interestig in a technical point of view.\nWhat's ironic is that it is only possible to achieve it thanks to... protections added to the game by the developpers\nin order to make cheating more difficult (in particular, a very basic kind of ASLR and some checksum verifications) 🤦‍♂️\nBut achieving ACE is not an easy task: you have to write some code in the memory, and then make the game execute it.\nThe latter is very exciting, but it is not the subject of the project I made. What I decided to make is a tool\nto achieve the former, that is, writing machine code (ARM7TDMI) in a specific location in memory. For that, we use a mechanic of the game\nthat allows us to rename boxes of the in-game PC (where we store our pokemons): it consists of 14 names of 8 characters each.\nThose 14 names are stored consecutively in memory, one byte for each character, but are separated by a 0xFF byte (the EOF character).\nThus, it takes in total (8+1)*14=126 bytes.\nThe main issue is that only about 1/3 of the 256 values possible for each byte can be written, due to the character encoding used by the game.\nSo, we have to write machine code (using one of the ARM or Thumb instruction sets), but by being unable to write 2/3 of the possible byte values...\nThat sounds like an impossible constraint! Fortunately, while it seems very complicated to write Thumb code with this constraint,\nit is possible, to write very interesting ARM opcodes: some arithmetic ones (ADC,SBC), and some memory-related ones (MOV,STR(H),LDR(H)).\nOf course, only a small subset of registers and immediate constants are accessible due to the constraint on the charset. But\nit is enough to write abritrary code: by doing the right arithmetic operations using MOV, ADC and SBC, we can obtain any opcode\nwe want in a register, and then write it a little ahead of the current instruction (PC register), using a command STR, for it to be executed.\nAnother constraint is the presence of the 0xFF bytes (EOF), which cannot be modified, at the end of each box name. It forces us to insert some dummy\nmachine instructions that do nothing but to contain this EOF. After that, we just have to convert the machine code we obtain into characters\nusing the character encoding, and we are done.\nThis whole process is what the tool I made automates! You can access it online\n(or view the source code, in OCaml, on Github). It parses some ARM assembly code written by the user (with some extensions),\nfinds a way to write immediate values using writable arithmetic operations, assembles them and encodes the result, for finally showing the\nbox names one has to enter in the game!\nUsing this code generator, it is also possible to setup a much more powerful ACE environment, for instance by bootstrapping a code that allows to get rid of the limitations cited above. You can take a look to this video I made that shows a full exploitation of ACE in order to inject a new Pokemon species in the game!\n" } , { "title": "Rom-hacking: level editor for Kuru Kuru Kururin", "url": "https://mlaurent.ovh/projects/kururin-editor/", "body": "In 2020, one year after the TAS of Kuru Kuru Kururin, I decided to investigate the code of this GBA game furthermore and make an editor\nthat allows to edit the maps of the game! Armed with an emulator and a debugger, I tried to document where and how maps are stored,\nto extract the tiles and palettes for each level, etc. Finally, I managed to make a level editor!\nYou can find it on Github (the source code is written in C#).\n\nMy friend mohoc7 used it to create an insane(ly difficult) ROM-hack that you can download here 😁\n(and it works on a real GBA: I've tested it!).\nI also adapted the level editor to support the sequel of the game, Kururin Paradise, with some contributions from Dimedime!\n" } , { "title": "Bot: the Gravitron of VVVVVV (DQN vs search-based)", "url": "https://mlaurent.ovh/projects/vvvvvv-bot/", "body": "The source code of the PC game VVVVVV\ngot officialy released in 2020. It was announced by my friend\nmohoc7, during his speedrun of this game\nat the AGDQ 2020.\nIt motivated me to dig in the source code and see what I could do... and I finally decided to make a bot for the Super-Gravitron (a mode of the game where we have to avoid projectiles)!\nI first made a Python bot using an implementation of a DQN in order to learn to play this game, as it was done by Google for some Atari games (link). For that, I customized the game a little in order to be able to feed it inputs from the console, and to output the current game state in the console too (Github).\nThen, a little deceived by the result (though it was performing way better than the average human, it did not break the ~10min record of my friend!),\nI decided to make another bot, this time without using machine learning.\nI replicated the physics of the game in Julia (for better performances than Python), and made a search-based bot. This time, the record was beaten... 💪\nYou can look the performance of both bots on this video, and the source code is available on Github.\n" } , { "title": "Tool Assisted Speedrun: Kuru Kuru Kururin", "url": "https://mlaurent.ovh/projects/kururin-tas/", "body": "In 2019, I made a Tool Assisted Speedrun (TAS) with a classmate and dear friend, mohoc7.\nYou can watch it, as well as read our comments and explanations, on tasvideo.org.\nWhile mohoc was the expert of the game and main director of the TAS, I was the technical team.\nIf you watched the video of the TAS, you might be thinking "well, this game is totally broken, look how it is easy to clip in the walls!".\nBut if you try it yourself, you might be surprised how difficult it is! Actually, clipping in a wall without the help of a moving object is\nnot humanly feasible: you need a tool that allows you to choose which button to press on every frame if you want a chance to replicate it.\nAnd even with such a tool, this is quite complicated: in fact, another TASer, Ryuto, made a TAS years before our,\nwithout even noticing such a mechanics was possible.\nSo, how to achieve it? You can find an explanation of how it works on tasvideo.org,\nbut the conclusion is that there is no systematic way to achieve it! It relies on a very precise combination of position, velocity\nand collision mask, and the only way we found in order to be able to achieve it in different places is to make a bot that tries a lot of paths.\nIt wasn't possible for that to make a script that communicate with the game in order to test different paths, because it would have been way to slow.\nInstead, I replicated the exact physics of the game, from the logics of collisions to the computation of trigonometric functions with the good precision!\nI implemented it in C#, and you can find the code on Github.\nIn order to search paths, I basically used an A* algorithm with a custom cost map computed with some kind of flooding algorithms.\nSome optimisations and approximations were necessary in order to reduce the search space, but in the end, it worked!\nThough, there is no guarantee of optimality in the results produced (not the full search space is explored, and the cost map is just an heuristic).\nBut anyway, that was a great challenge, both algorithmic and technical, and I really like the result 😁!\n" } , { "title": "Polymorphic Type Inference for Dynamic Languages", "url": "https://mlaurent.ovh/publications/polymorphic-type-inference/", "body": "Giuseppe Castagna, Mickaël Laurent, Kim Nguyen & Matthew Lutze\nWe present a type system that combines, in a controlled way, first-order polymorphism with intersectiontypes, union types, and subtyping, and prove its safety. We then define a type reconstruction algorithm that issound and terminating. This yields a system in which unannotated functions are given polymorphic types(thanks to Hindley-Milner) that can express the overloaded behavior of the functions they type (thanks tothe intersection introduction rule) and that are deduced by applying advanced techniques of type narrowing(thanks to the union elimination rule). This makes the system a prime candidate to type dynamic languages.\nView PDF\n" } , { "title": "On type-cases, union elimination, and occurrence typing", "url": "https://mlaurent.ovh/publications/on-typecases-union-elimination-occtyping/", "body": "Giuseppe Castagna, Mickaël Laurent, Kim Nguyen & Matthew Lutze\nWe extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing. To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.\nView PDF\n" } , { "title": "Revisiting occurrence typing", "url": "https://mlaurent.ovh/publications/revisiting-occtyping/", "body": "Giuseppe Castagna, Victor Lanvin, Mickaël Laurent & Kim Nguyen\nWe revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages. Although occurrence typing was tied from its inception to set-theoretic types—union types, in particular—it never fully exploited the capabilities of these types. Here we show how, by using set-theoretic types, it is possible to develop a general typing framework that encompasses and generalizes several aspects of current occurrence typing proposals and that can be applied to tackle other problems such as the reconstruction of intersection types for unannotated or partially annotated functions and the optimization of the compilation of gradually typed languages.\nView PDF\n" } , { "title": "Merit and Blame Assignment with Kind 2", "url": "https://mlaurent.ovh/publications/merit-and-blame-assignment-kind2/", "body": "Daniel Larraz, Mickaël Laurent & Cesare Tinelli\nWe introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, guarantees, or other behavioral constraints in synchronous reactive system models. This new version of Kind 2 can identify minimal sets of design elements, known as Minimal Inductive Validity Cores, which are sufficient to prove a given set of safety properties, and also determine the set of MUST elements, design elements that are necessary to prove the given properties. In addition, Kind 2 is able to find minimal sets of design constraints, known as Minimal Cut Sets, whose violation leads the system to an unsafe state. We illustrate with an example how to use the computed information for tracking the safety impact of model changes, and for analyzing the tolerance and resilience of a system against faults.\nView PDF\n" } ]