<\/a><\/p>\nThese classical methods of testing can be thought of as internal testing: the test routines access the internal representation of the data structures to be checked. We propose a new method of external testing where the library only deals with a module interface. The data structures are exported as abstract types; the testing framework behaves like regular client code and combines functions exported by the module to build new elements of the various abstract types. Any counter-examples are then presented to the user. Furthermore, we demonstrate that this methodology applies to the smart-fuzzing of security APIs.<\/p>\n
I work for a start-up, work on hardware security models (HSM). Some hackers have been about to steal lots of money due to issues with HSM.<\/p>\n
Cryptosense Workflow<\/p>\n
Testing -> Learning -> Model-checking -> ...<\/p>\n
We will focus on Testing, we automatically test API's using QuickCheck (a combinator library to generate test case in Haskell), But to generate tests we need to know how to generate our types\/data structures.<\/p>\n
ArtiCheck - a prototype library to generate test cases for safety properties. Comparison of QuickCheck of ArtiCheck.<\/p>\n
Types help us to generate good random values, API's help generate values that have the right internal invariants.<\/p>\n
Well-typed does not mean well-formed so we still need fuzzing.<\/p>\n
Describing & Testing API's, we are only considering on first order functions.<\/p>\n
Example of how we would test an example of API for red black trees.<\/p>\n
Introducing a toy DSL for describing API's: describing types, functions and signatures.<\/p>\n
There are many ways to combine these functions. so we introduce a richer DSL for types.<\/p>\n
Field Report: Cryptosense
\nWe need to enumerate a big combinational space made of constants and variables. We want good coverage and generate templates in a principle manor.<\/p>\n
We have a library of enums with a low memory footprint with efficient access.<\/p>\n
We have another DSL for describing combinatorial enumeration.<\/p>\n
Example test results from a HSM. We have 10^5 test in 540 secs.<\/p>\n
We have a principled way to test persistent APIs.<\/p>\n
Writing a generator for testing BDD would be very tough without solutions like this.<\/p>\n
Come work for Cryptosense :)<\/p>\n
Q: How long does it take run the data on a real HSM ?
\nA: the numbers show actually already include already, we dynamically explore the state space.<\/p>\n
Q: How do you trade-off coverage of API to coverage of state space ?
\nA: You a systematic approach. e.g. constantly generate trees which are bigger and bigger, so you don't just regenerate empty trees.<\/p>\n
Q: Can you find a simple counterexample like QuickTest ?
\nA: Its not currently a function but maybe we can add a function to find an example smaller that exhibit the same behaviour<\/p>\n
Q: Is this open source ?
\nA: Yes, the prototype is on github<\/p>\n
Improving the CakeML Verified ML Compiler (Research presentation)<\/h4>\nRamana Kumar; Magnus O. Myreen (University of Cambridge); Michael Norrish (NICTA); Scott Owens (University of Kent)<\/h4>\n
Abstract: The CakeML project comprises a mechanised semantics for a subset of Standard ML and a formally verified compiler. We will discuss our plans for improving and applying CakeML in four directions: optimisations, new primitives, a library, and verified applications.<\/p>\n
Introducing the CakeML team, we are verification people.<\/p>\n
Why ML for verification: its clean and high level, its easy to reason about so can we then formally reason about it.<\/p>\n
CakeML: a subset of ML which is easy to reason about, with verified implementation and demonstrate how easy it is to generate verified cakeML<\/p>\n
How can we make proof assistant into trustworthy and practical program development platforms.
\nfunctions in HOL -> CakeMl -> Machine code<\/p>\n
2 part to this talk:
\n- verified compiler
\n- making the compiler better<\/p>\n
Highlights of CakeML compiler:
\nMost verified compiler work from source code to AST to IR to bytecode to Machine code. We take a difference approach and can do both dimensions in full.<\/p>\n
The CakeML language, its SML without IO and functors. Since POPL '14 we've added arrays, vectors, string etc..<\/p>\n
Contributions of POPL '14 paper: specification, verified algorithms, divergence preservation and bootstrapping. Proof developer where everything fits together.<\/p>\n
Numbers: its slower, our aim is to be faster then interpreted OCaml.<\/p>\n
The compiler phases are simple, we use only a few hops from IR to x86. Bytecode simplified proofs of real-eval-loop but made optimisation impossible.
\nWe are now add many more IR's to optimise, like common compilers. Currently we only have x86 backend but we are adding ARM etc..<\/p>\n
C: Inlining and specialisation of recursive functions are the key optimisations that you should focus on<\/p>\n
C: You could use your compiler (written in cakeML) to evaluate the value of various optimisations<\/p>\n
Q: Why don't you support functors ?
\nA: Its not a technical issue, this just a lot of work and its at the top of the priorities stack.<\/p>\n
C: Your runtime value representation could make a big performance issues<\/p>\n
C: Can you eliminate allocation in large blocks<\/p>\n
\n<\/h4>\nSession 3: Beyond Hindley-Milner<\/h4>\nChair: Jacques Garrigue<\/h4>\nThe Rust Language and Type System (Demo)<\/h4>\nFelix Klock; Nicholas Matsakis (Mozilla Research)<\/h4>\n
Abstract: Rust is a new programming language for developing reliable and efficient systems. It is designed to support concurrency and parallelism in building applications and libraries that take full advantage of modern hardware. Rust's static type system is safe and expressive and provides strong guarantees about isolation, concurrency, and memory safety.<\/p>\n
Rust also offers a clear performance model, making it easier to predict and reason about program efficiency. One important way it accomplishes this is by allowing fine-grained control over memory representations, with direct support for stack allocation and contiguous record storage. The language balances such controls with the absolute requirement for safety: Rust's type system and runtime guarantee the absence of data races, buffer overflows, stack overflows, and accesses to uninitialized or deallocated memory. In this demonstration, we will briefly review the language features that Rust leverages to accomplish the above goals, focusing in particular on Rust's advanced type system, and then show a collection of concrete examples of program subroutines that are efficient, easy for programmers to reason about, and maintain the above safety property.<\/p>\n
If time permits, we will also show the current state of Servo, Mozilla's research web browser that is implemented in Rust.<\/p>\n
Motivation: We want to implement a next gen web browser servo<\/p>\n
See the rusty playpen online http:\/\/www.rust-lang.org\/<\/p>\n
We want a language for systems programming, C\/C++ dominate this space. We want sound type checking. We identify classic errors and using typing to fix them.<\/p>\n
Well-typed programs help to assign blame.<\/p>\n
Systems programmers want to be able to predict performance.<\/p>\n
Rust syntax is very similar to OCaml. Types have to explicit on top-level functions. Rust has bounded polymorphism, we don't have functor, this is more similar to typeclasses.<\/p>\n
Value model between OCaml and Rust is very different. Rust in-lines storage but must pick the size of the largest variant.<\/p>\n
To move or copy ? Move semantics<\/p>\n
The Copy bound expresses that a type is freely copyable and its checked by the compiler.<\/p>\n
Many built-in types implement Copy<\/p>\n
Why all the fuss about move semantics ?
\nRust has 3 core types: non-reference, shared reference, mutable unaliased reference. (plus unsafe pointers etc..)
\nRust patch matching moves stack slots. Rust introduces ref pattens and takes references to its interioa.<\/p>\n
This is all more type soundness<\/p>\n
Q: Is borrowing first order ? Can I give to someone else ?
\nA: Yes, I'll explain more later<\/p>\n
Lifetimes: simulator to regions used by Tofte\/Talpin<\/p>\n
Example of sugar and de-suger forms of functions: how we can explicitly constrain lifetimes<\/p>\n
Is every kind of mutability forced into a linearly passed type ?
\nNot really, there's inherited and interior mutability.<\/p>\n
Rust has closures<\/p>\n
Q: Does rust repeat earlier work on cyclone ?
\nA: Cyclone tried to stay very close to C but we more then happy to diverge from C\/C++<\/p>\n
Q: Large scale systems code becomes tanted with linearity, how do you deal with that ?
\nA: You can break out of it, only very occationally need to break into unsafe code<\/p>\n
Q: How do you know that your type system is safe ?
\nA: There's ongoing work<\/p>\n
Doing web-based data analytics with F# (Informed Position)<\/h4>\nTomas Petricek (University of Cambridge); Don Syme (Microsoft Research Cambridge)<\/h4>\n
Abstract: With type providers that integrate external data directly into the static type system, F# has become a fantastic language for doing data analysis. Rather than looking at F# features in isolation, this paper takes a holistic view and presents the F# approach through a case study of a simple web-based data analytics platform.
\nExperiments can have a life of its own independent of a large-scale theory. This is a relevant case study, theory and language independent and demonstrates a nice combination of language features<\/p>\n
Demo: demo using type providers and translation from F# to JS.<\/p>\n
Features used: type providers, meta-programming, ML tyoe inference and async workflows.<\/p>\n
JS Intergration: questions on whether to use JS or F# semantics.
\nAsynchronous workflows - single thread semantics<\/p>\n
Not your grandma's type safety,<\/p>\n
Q: These language feature are good for specific application, do they make the language worse for other features ?
\nA: No the extensions use minimal syntax<\/p>\n
Q: Is there version contrainting on type providers for data source ?
\nA: No<\/p>\n
<\/p>\n
The rest of the posts will follow soon<\/p>\n
<\/p>\n
\n <\/p>\n
Session 4: Implicits <\/b><\/p>\n
Chair: Andreas Rossberg<\/b><\/p>\n
Implicits in Practice (Demo) <\/b><\/p>\n
Nada Amin (EPFL); Tiark Rompf (EPFL & Oracle Labs)<\/b><\/p>\n
Abstract: Popularized by Scala, implicits are a versatile language feature that are receiving attention from the wider PL community. This demo will present common use cases and programming patterns with implicits in Scala.<\/p>\n
Modular implicits (Research presentation) <\/b><\/p>\n
Leo White; Fr\u00c3\u00a9d\u00c3\u00a9ric Bour (University of Cambridge)<\/b><\/p>\n
Abstract: We propose a system for ad-hoc polymorphism in OCaml based on using modules as type-directed implicit parameters.<\/p>\n
\n <\/p>\n
Session 5: To the bare metal <\/b><\/p>\n
Chair: Martin Elsman<\/b><\/p>\n
Metaprogramming with ML modules in the MirageOS (Experience report) <\/b><\/p>\n
Anil Madhavapeddy; Thomas Gazagnaire (University of Cambridge); David Scott (Citrix Systems R&D); Richard Mortier (University of Nottingham)<\/b><\/p>\n
Abstract: In this talk, we will go through how MirageOS lets the programmer build modular operating system components using a combination of functors and metaprogramming to ensure portability across both Unix and Xen, while preserving a usable developer workflow.<\/p>\n
Compiling SML# with LLVM: a Challenge of Implementing ML on a Common Compiler Infrastructure (Research presentation) <\/b><\/p>\n
Katsuhiro Ueno; Atsushi Ohori (Tohoku University)<\/b><\/p>\n
Abstract: We report on an LLVM backend of SML#. This development provides detailed accounts of implementing functional language functionalities in a common compiler infrastructure developed mainly for imperative languages. We also describe techniques to compile SML#'s elaborated features including separate compilation with polymorphism, and SML#'s unboxed data representation.<\/p>\n
<\/p>\n
\n <\/p>\n
Session 6: No longer foreign<\/h4>\nChair: Oleg Kiselyov<\/h4>\nA Simple and Practical Linear Algebra Library Interface with Static Size Checking (Experience report)<\/h4>\nAkinori Abe; Eijiro Sumii (Tohoku University)<\/h4>\n
Abstract: While advanced type systems--specifically, dependent types on natural numbers--can statically ensure consistency among the sizes of collections such as lists and arrays, such type systems generally require non-trivial changes to existing languages and application programs, or tricky type-level programming. We have developed a linear algebra library interface that guarantees consistency (with respect to dimensions) of matrix (and vector) operations by using generative phantom types as fresh identifiers for statically checking the equality of sizes (i.e., dimensions). This interface has three attractive features in particular.<\/p>\n
(i) It can be implemented only using fairly standard ML types and its module system. Indeed, we implemented the interface in OCaml (without significant extensions like GADTs) as a wrapper for an existing library.<\/p>\n
(ii) For most high-level operations on matrices (e.g., addition and multiplication), the consistency of sizes is verified statically. (Certain low-level operations, like accesses to elements by indices, need dynamic checks.)<\/p>\n
(iii) Application programs in a traditional linear algebra library can be easily migrated to our interface. Most of the required changes can be made mechanically.<\/p>\n
To evaluate the usability of our interface, we ported to it a practical machine learning library (OCaml-GPR) from an existing linear algebra library (Lacaml), thereby ensuring the consistency of sizes.<\/p>\n
SML3d: 3D Graphics for Standard ML (Demo)<\/h4>\nJohn Reppy (University of Chicago)<\/h4>\n
Abstract: The SML3d system is a collection of libraries designed to support real-time 3D graphics programming in Standard ML (SML). This paper gives an overview of the system and briefly highlights some of the more interesting aspects of its design and implementation.<\/p>\n
Closure<\/h4>\n
and we headed of to the ICFP Industrial Reception ...<\/p>\n
<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"Welcome to the ML Family workshop liveblog with Leo, our guest blogger\u00a0Gabriel Scherer and myself. Welcome Welcome, this year we worked closely with the OCaml workshop to give the two workshops they’re own focus, this workshop is more theory focused then the OCaml workshop. This workshop doesn’t just include features in current SML, but also […]<\/p>\n","protected":false},"author":35,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[29,30],"tags":[],"_links":{"self":[{"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/posts\/1827"}],"collection":[{"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/users\/35"}],"replies":[{"embeddable":true,"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/comments?post=1827"}],"version-history":[{"count":8,"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/posts\/1827\/revisions"}],"predecessor-version":[{"id":2359,"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/posts\/1827\/revisions\/2359"}],"wp:attachment":[{"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/media?parent=1827"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/categories?post=1827"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.syslog.cl.cam.ac.uk\/wp-json\/wp\/v2\/tags?post=1827"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}