Crema: A LangSec-inspired Language

I

flew all the way from Luxembourg to see from Las Vegas thank you we good okay thank you and welcome everyone my name is Jacob Tori and my co speaker Sergei brought us unfortunately could not be with us but this is our work we just finished up for DARPA I 20 it's called crema which is a Lang sec inspired programming language so we're going to go through kind of the problems and kind of the Lang sec kind of theory about what those problems stem from how to propose a solution we're going to talk about crema specifically which is one kind of piece of that solution and then talk about some of the results we found or the paper that's actually out in the

I Triple E security privacy journal and then some other kind of interesting stuff before we wrap up because it's a very mixed audience and this can be you know very basic in some fields but also quite you know advanced in some of the more theory stuff if you have a question any point please just raise your hand and jump in if you'd something as is unclear I gave a talk here last year and I said the same thing at the very beginning and I didn't get any questions and I stop part way through I said any questions I still no questions the very end any questions no questions okay we'll see at the bar and everyone got up

and lined up to ask me questions that they were too embarrassed so don't be those people please just ask so so basically in a nutshell you know programming languages provide more computational power or more expressiveness than most programmers need and so lange sec has shown that this excess you know within that kind of you know skin around the the orange is where you have these weird machines verification difficulties when you're trying to formally verify and prove out your software and then also a state-space explosion when you're trying to do program analysis so we're hoping that by providing a language that forces programmers to more accurately express their intent and to basically had a right size the programming language to

most tasks will be able to show some security wins so I work for a shirt information security out in Colorado I leave the computer architectures group this is actually kind of an aside for me usually I'm doing hypervisor research or operating system security and Sergei is a professor out at Dartmouth he's come one of the kind of visionaries behind the Lang SEC field he's a chair of the laying sec conference out at I Triple E unfortunate had to miss it last minute so but you can reach out to both of us on Twitter if you have any questions or you want to get interested in the Lang SEC dialogue there's a great mailing list it's quite low traffic but very

very interesting so a couple definitions just so we're kind of all know where we're on the same page so turn complete basically if a system for program if a machine can simulate the widely known Turing machines you have a tape with you know input output and then you can read through it basically computers today are finite physical implementations of it so technically a computer is not a Turing machine because eventually the heat death of the universe will cause it to terminate and also it's not infinite but for all intents and purposes you can think of a program kind of assimilating that and turn completeness shows up in some of the most bizarre places so Sergei and Julian Bangert showed that

the Intel memory management unit itself is turing-complete so without ever executing an instruction on x86 CPU you can actually simulate any program or any Turing machine just by setting up and triggering these memory errors at the right time and the interrupt logic is so complicated you can simulate any Turing machine without executing a single instruction it shows up all over the place and it's kind of a very nasty thing to try to work around and analyze and verify because of the halting problem so this is kind of a classic problem computer science that is provably undecidable in general to determine if kind of any program hults on a given input and there's a proof for this using cantor

diagonalization which we won't get into but basically you run into this issue once you get to a certain class of computational power it's also known kind of is the undecidability cliff so the more complicated environment you have the more difficult is to analyze eventually you kind of reach this cliff where everything more advanced in that just kind of falls off the cliff and it's kind of impossible to recover from this is kind of more granularly codified in the Chomsky hierarchy which just shows kind of here you'll see formal language classes and then the machines that can basically represent them so you have very very simple finite state autonomous finance state machines that can recognize and accept regular

languages and then you go all the way up to context-sensitive context-free and then all the way up to Uncle and so you'll see here that basically there's a levels of complexity and then also there's machines that can accept it and then they actual grammar class itself so lange second a nutshell this is a very long but essentially when you n handle input in kind of loosey-goosey ways you're opening yourself up to whole set of problems if you were to formally verify and parse your input to the same degree of certainty that a compiler does for example if you leave a semicolon off on your compiler it'll throw up at you because you didn't meet the formal

grammar for whatever language you're programming in most input handling for data doesn't have that same level of exactness and because of that you get a whole bunch of these kind of weird machines which are essentially virtual machines of the Java VM not the vmware vm type that runs some weird instruction set architecture that's defined by your data and so you can turn data to drive execution and so with lang sec if you take you know software that basically formalizes the specification for the input language and rejects anything outside of that you're going to basically remove a whole class of attack so that was great so basically we built the internet on faith that developers will properly sanitize their inputs

they'll think of all possible kind of edge cases and though you know you know correspond and work against that and then we've trusted them to the full power of Turing completeness it's kind of like giving your sixteen-year-old kid who's never driven before a Ferrari because that's pretty much the most powerful car and why would you want anything less powerful why would you give them an accord and between this Ferrari and follow the breaches we see kind of on a day-to-day basis and everything coming out from project zero maybe that faith that we place in developers might have been a little bit miss found especially since the large majority of tasks don't require a Ferrari just commuting to work

doesn't require a Ferrari whereas maybe driving on a track does so this is trying to write size down the language to something that you know maybe we'll make it a little bit harder for programmers to shoot themselves in the foot so this is some of Sergei's kind of a thing where you have code that meets input the code goes crazy and then it elopes beyond your wildest expectations it's very fitting we are in Las Vegas and here we have I bet there's probably an Elvis wedding in there as well which you could probably say return oriented programming would be that so essentially with returning to programming your data which is return addresses ends up being

kind of an assembly language for this virtual machine and you're able to derive execution flow from data the other issue if this is that static analysis are very very difficult to kind of in a general sense kind of classify and then actually prove and so we're going to talk about that some specific examples a little bit later but essentially you get to the point where if you have two parsers that should recognize the same input it's typically undecidable whether or not they're the same and so you'll see this issue with there was a just a bitcoin bug in the Bitcoin protocol where they had separate interpretations of the asn.1 standard for certificates and so if you were

running it on a 32-bit system you would think the transaction was invalid but if it was a 64-bit system you'd think the transaction was valid and so that would create these kind of splits and forks in the block change or based on the CPU architecture and so being able to verify that basically both versions on both systems were kind of in sync is pretty difficult to do and so that's where you get these weird machines which are kind of these strange computation of virtual machines that kind of comes from that surprising comput eight Turing completeness from the memory management it shows up the BGP routing protocol is actually a distributed Turing machine you can actually program the worldwide vgp

network by making certain requests you can set up like a circuit and then kind of from that build all the way up to a distributed machine and so you kind of is very very easy to end up in Turing completeness which is kind of strange because they have all these languages like brainfuck or bull which try to say oh we're the smallest turing-complete language which you want to be I want to see the biggest language is not turn complete because there's a whole host of kind of problems that come with Turing completeness so there's a basically this is a great quote I'm just going to say the illusion that your program is manipulating data is powerful

it's an illusion the data is controlling your program your input is driving execution and maybe not necessarily in the sense that you know your CPU is running your data per se but it is driving execution flow and any input is a program and so this is where I talked about that if you have a you know a complex data format how do you distinguish between something like a java bytecode or a rock bytecode and then your actual your proper data format and so you have these weird machines it's jump up there basically virtual machines that execute this complex data format and they derive execution and so one great example this is the PDF spec PDF spec is very very complicated it's

actually possible to make a PDF that has a cyclical reference for length and until they put in a special edge case for this you could actually send some of the PDF that would just loop forever and then crash and so PDF spec is very very complicated and so it's essentially it has the ability to flat out just embed JavaScript and other code into a PDF which is a terrible idea so that point you know what's the point of having all this other stuff you're are you're letting people write code why bother basically make it really easy so basically there's a gap now right so we've shown that basically it's pretty scary out there but a lot of what we

need is necessarily require all that kind of scary world and so there's a huge gap between what programmers need for both tasks so i would say many tasks you probably want your program to terminate or at least generate input from our output from input and so typically you want your program to kind of have some bound on its execution there's a few examples counter examples to that which I'll talk about later but you know there's a whole bunch of things here that you know get in the way so there's a lot of CPU features there's a whole bunch of crazy programming language stuff so like the you know the percent and the percent s there's a

whole bunch of format character string weirdness and then also optimizing stuff as well so you can bring it all the way back to reflections on trusting trust where you have all these layers you have kind of abstraction and so what we're trying to do here is if you create your data specification as strictly as your code specification when you're writing your code you should be able to kind of have predictable computation and be able to you know really cleverly analyze it so our approach is to limit the power of the processor or in this case the execution environment I'm actually talking with some folks from Intel about kind of reusing some cpu flags to be

able to actually create a limited kind of execution mode kind of like ring three you could make like a ring for which is then kind of computationally limited which then gives you better predictability and then it's you know basically a language that's deliberately not Turing complete and so it's going to require a little bit more thinking from the developer standpoint because they need to figure out exactly what they're trying to do and they can't just kind of use a Ketchel and so i'll talk about a bug in sendmail that marked out found which basically showed that a programmer was not necessarily thinking about the full intent of what they were trying to do and because of that they had kind of

some extra edge cases that allowed remote code execution so our goal is is we want to make something that ends up being accidentally turn complete we don't never want that to happen we're trying to make it so that the programmer has to think through what they're trying to do and make it such that it's never going to end up kind of in this undecidability cliff we're talk about least privileged principle as it opposed to computational power so one of the interesting things about this is typically when malware first came out it would be running in user space and your anti-malware would be a kernel mode driver and so it can kind of look down it has more power than

the malware and it can pretty easily find it so what did a lot of malware people do they found ways to hop up into the kernel and now they're kind of playing on the same space and so now there's you know a V and next generation whatever fire I stuff that runs in hypervisor land but at the same time now it's a matter of time before malware start hopping up into V mmm this is the same thing with reference monitors and programs right now you might have some reference monitor that's checking a program as is executing to make sure that it's not doing something bad but that's operating in the same kind of computational privilege level as the

program it's analyzing and so you can think of a reference monitor is essentially an automaton that recognizes a series of inputs from events basically so it's watching the program and if it starts seeing these events that it shouldn't recognize it can use a prefix since they are everything past that is bad and then it can hold the program if you had a provably halting execution you'd be able to do a much stronger both prefix and postfix your kind of all encapsulating you'd actually be able to run a computation see if it matched some malicious characteristic and then actually roll it back as a whole because you have kind of this computational transaction so Meredith Patterson who

also couldn't be here unfortunately at a pretty good quote so your CPU has to be able to perform arbitrary computation the echo request doesn't so allowing like basically a full virtual machine to run anything in your network stack is probably not so good and you sometimes see this stuff especially with actually asn.1 parsing which is used a lot in HTTPS TLS SSL where you just have these very kind of arbitrary computations and very very complex computation that need to be done just to parse input and say your CPU has all this power and programmers are kind of letting it at it so that's a pretty poignant quote so the sub Turing programming language that we're going to

developer I'm going to magically it's like a cooking show we're going to talk about what we're going to make and then in the next slide it's already going to be made so basically we want to make it really really hard to express what's hard to analyze so from a program verification standpoint you know bugs are always going to happen developers are not bad they're not you know dummies they just something to make mistakes you have deadlines you got to work and you got to do your thing and so a lot of times also you have feature creep or you were told this is just going to be a prototype and it's going to be scrapped

and then rewritten in beautiful codes you hack it together and they're like oh yeah let's push to production we're good so people who are chuckling have probably worked in similar companies so you want to basically compile this program to an execution model where things that are hard to analyze are ambiguous are kind of hard to program to and we wanted to make sure that it can represent we'll see well enough because programmers don't fall from the sky they have to learn making this language open source and you know DARPA investing in this doesn't make sense if only three PhDs in the world can program I don't have a PhD so I'm one of the people who

is not a PhD they can program in it but we really want to make sure that it's kind of easy to use so that you could actually start including it in at least portions of your program so apparently crocodiles I learned this don't turn around so if you imagine a processor that never went backwards so you have no loops you have no turn completeness and then you combine it with basically upper limit so Captain Hook would have a much easier time of aiding from a bounded execution crocodile apparently the crocodiles name is tik-tok I learned that today so just kind of an aside there a Sergei thought that was had to be included so there it is

so basically all these questions and concerns is basically all right so we've been developing software for a very long time and it seems like there are some edge cases that the software has been kind of a knife able to stand withstand the test of time but there's also a lot of cases where that clear hasn't been the case and so we started a DARPA seedling under I 20 which is their information operations group we tried to figure out what the minimum kind of cover set for the majority of programming tasks were obviously we knew we couldn't do everything but we wanted to be able to figure out okay what are most programming tasks do and a lot of

those are basically parsers or we call transducers they take input from some format and provide output that could be something like a USB mass storage driver it takes input from the USB bus which is basically data being loaded into memory mapped i/o space it parses that into essentially scuzzy and then it passes off to another driver which takes scuzzy to BFS and then BFS too fat or EXT and co just chains of parsers that all themselves should terminate and you can kind of put a bound on it based on though you know some polynomial function of the size of the input so if you kind of basically make this programming language provably terminating and countable time so that's what's known as

Walter recursion you have no issues with the halting problem so you've been able to kind of sidestep that huge issue with a lot of verification and programming tasks the programming language forbids unbounded loops and unbounded recursion or co recursion so that's if you have function a that calls function B and then be back to a so that's kind of a trick you might be able to break out oh so you explicitly prevent that at compile time we wanted to make sure it's very usable and embeddable so we actually emit lvm intermediate representation code so you can link to it and call from it and optimize it the same way as any of your other source

code so if you're writing xcode and you're writing a parser say in a program you're writing for OSX because that uses si lang to compile down to your representation you'd be able to write your parsers in crema and have a pretty high degree of confidence in them and then just kind of you know call parse data from see if you need to do some crazy graphic stuff and we try to make it easy to develop in a pretty small learning curve this is still an ongoing effort and we're working on getting some follow-on to make it even more easy to use people are I think C is a great language to learn and very easy but it seems like the

common trend in computer science programs is that Python or Java is an easy language and that so we're trying to make it as easy to learn as possible just because if the developers who are maybe struggling to learn and understand the nuances of see our learning crema at least they have a little less rope to hang themselves with so obviously it's not the right tool for every tasks there are some programming tested just flat-out require full computational expressiveness so anything with unbounded looping that requires unbounded looping so imagine if you had your OS scheduler that you had to put a bound on so your Linux system you boot it up and then after five minutes it

just forcefully shuts down because after that you're done you're out of time so that would be pretty frustrating it'd almost be like running XP when they shut your system down when you have an update without telling you oh yeah we just we're not going to save your stuff either don't worry so you know so and also you have a lot of kind of server listen loops so you know Apache has this loop that just listens on a certain socket and then Forks off or worker threads essentially when it gets a request those worker threads what they should do is probably be sub Turing you don't want a website take forever to render but the thing that's listening

there should basically go on and for a very long time and a lot of user driven programs the UI side of it typically are multi-threaded anyways because you have your UI thread that allows a year to click on a whole bunch of stuff and then the background processing and so the background processing would be something that you'd want to be bounded but the actual you know waiting for the user could go on for a long time and you can actually see this model in the real-time fork of Linux you have kind of your tight loop and then you have these little task list in the colonel you also see this in Windows kernel programming you have like a top end and a bottom end

you know interrupt handler and so basically the top end says there's a lot of work to be done here but a lot of people are waiting for me so I'm just going to queue it up for later figure out what's the least important stuff and do it later and so you kind of already have this kind of system set up just a matter of really limiting those parts that are already could be limited and since chroma you know it is very easily to embed you have a lot of parsers and data analysis methods in llvm and you can really compose this really well like you can take crema file and a C file and compile them down to

the same binary so it's strongly typed to see like language as I mention you can use the lvm to call into or be called from other languages you can have structures that can pay pass back and forth and it can express anything that's known as a parser or a transducer which essentially converts input from one format to another which seems like a very very small use case but if you think about how you organize your program it's actually very very common a kind of design pattern these transducers or parsers basically should take a polynomial time function with respect to the input length or the input complexity and that should not be undecidable and so this is kind of how you are able to

calculate the bounds in real time so this is grandma doesn't look too crazy essentially we have an array of ince called 100 so the crema seek basically generates a sequence like in Python with between one and a hundred this is the fizzbuzz like programming challenge I'm sure you've all seen it and some interview or joel on software and then basically you're just for each looping through it so this is a very straightforward you know fizzbuzz right here looks pretty similar other than the kind of ugly imprint and string print separate line thing but that's something else we're trying to clean up a little bit but for the most part it's pretty kind of approachable some of the other

kind of turn complete or sub turing-complete languages out there that have been built in the academic world are almost like unpossible by people who are just normal developers so we tried to make it something that's pretty approachable and pretty easy to learn so it supports you know your typical stuff struck raise the lists and arrays automatically scale so you can just append stuff to list if you need to obviously you can't upend stuff to lists that you're iterating through because then you keep ending to the next one but memory is automatically managed that you have all your normal bulleen and bitwise operators your main looping construct is for each and if you just want to do kind of a constant time you

can just throw in a sequence generator so creamy sec 1 2 3 will generate one two three so you can make an easy kind of loop in that way so it's still pretty young we spent about maybe four months working on it we're looking for input from anyone this is kind of its first release out to people who are not academic and who might actually consider using it or have features they miss so we have some future work that we want to do or no object oriented classes that kind of stuff is really good for representing kind of hierarchies of data and functions what we think would be really interesting is actually integrating a parser generator kind of

like lecture yak but specifically designed for not necessarily code but for data into it as the only method for reading input so imagine if you took C++ and you removed see in and you have to specify basically a you know format and like say BNF for what you're trying to recognize which are then automatically generate something that would reject any invalid input right there you basically make C++ like bulletproof and so we're trying to figure out a way that we could be able to take that so that you back to think about what you're trying to accept because typically you think about return to accept and you don't try to think about what you're not trying to accept

and it's all those edge cases that weren't in your mind that an attacker will be able to exploit we want a much stronger standard library you know programming in Python is like so easy do they have everything for you it's like our PHP just add like what you're trying to do an underscore with underneath it like write a compiler underscore and then boom it just does it so we also want to do some cleaning up so you know right here kind of the imprint and string prints kind of ugly we want to make some kind of syntactic sugar to really clean that up I'm and type conversion is a little ugly right now too so so here if anyone of you guys are

theoretical geeks basically we took the formal definition of a Turing machine and weary implemented the transition function which is basically the same except that it can't visit the same state again so essentially it's going to run out of states and so basically all it's exactly the same except that you know Q prime is a new set of states it has the current state removed from it so it can't loop back to itself so it's same Turing machine model if you guys are taking a picture of the slides I'm going to post them online that saves you some effort but and the video so all right so this is a very pretty when you type set it

and litec which probably build a reason to write in the tech because it's very pretty but what does it actually mean so imagine a CPU they can only execute for words so say to higher memory addresses you'll never be able to jump back and so if you have that program that you're right and you line it all up you know from the first instruction all the way the last instruction that program will terminate because eventually you'll hit the end of the program or the end of your memory your finite memory and it will terminate so you can actually compute how long that's going to take and that basically enforces you're bound on the state space explosion to verify

if you're doing some program analysis he's basically count the number of branches in between the startup program in the end of the program and massive number of possible states this is going to terminate unfortunately this removes all kind of powerful things like looping or function calls which as a developer I kind of like that would be really annoying to copy and paste your program so this is this kind of theoretical model that we used in our paper to kind of create the formalism this is not actually how crema work we don't put the CPU in a special mode we just can't do it a compile-time but think about how this is equivalent to crema as we go

forwards so we kind of introduce this work called basically just in time loop unrolling and so you imagine that you have your program which is kind of this abstracted model of a program that has the loop kind of like the the body of that loop abstracted you have all the functions that are they're kind of like p is and then you just in time assemble it once you know the length of your input and so say you're going to loop through your input twice to do something you can then basically go in and you can unroll the loop twice this is not actually happening this is really inefficient but for the formalism let's think let's

assume that happens so you're going to have your abstract program you're going to do just in time kind of compilation or loop unrolling and function insertion and then you're going to end up with a very very long and inefficient forward only execution program which then you can formally verify and then you can basically put in kind of random input lengths if you'd like to kind of do some analysis on an abstract sense now this supports walther recursion which essentially is as long as you can compute how many loop iterations there are as some function of the input this model with the Justin time loop unrolling will be able to support that while still running in that very very

constrained forward only execution model and so essentially you are doing the just-in-time unrolling before you're running the program and then you're doing your verification afterwards you can still have that very pleasant kind of bounded space to verify but you have a little bit more powerful as a program so your program analysis will operate on the forward only execution but when you're actually developing your kind of in this kind of play abstracted world which is more powerful than the forward only model so as kind of mention this but crema CC you could have output a program like a binary for whatever at platform you're on since its using llvm it can support x86 64 bit arm it can run

both just in time compiled compile down to whatever platform you're running on or also it can be interpreted but then also you can have it output as this kind of lvm assembly code which is an intermediate representation and then you can kind of bed it in other stuff so the ideal would be to use crema kind of right off the bat for anything that's input driven or parsing and then you can use your existing language and kind of deal with that kind of cleaned up data that you've already kind of got from crema you can call into other languages but that will break your guarantees if you call like while one from see that's obviously going to to break those

guarantees and the nice thing with lvm is that it already has a huge tool chain of compiler optimizations verification tools so CLE we used in our paper there's also some of the stuff that has a static analysis in xcode the sea lang and says a lot of tools that kind of just pick up this and once we're in that format can do some optimizations as well for performance benefit all right q male

DJ B is a generally considered a very competent programmer he wrote a male Damon called Q mail which was designed for security and he basically I think it's one of the first bug bounties I've seen he basically said I'll pay out of my own pocket kind of like Donald Knuth did with his if you find a typo in my book he's been all pay you you know some amount of money if you find a bug in it he's had this open for years and has been won award which was fairly minor and so it's been generally standing the test of time Pulver flake or Thomas Julian and Julian van egg have basically been using this back and forth in

conferences as targets basically how would we use automatic exploit generation what tools are needed to get automatic exploit generation to the level where we be able to actually target something like this and so Julian has basically these kind of like core requirements of things that we haven't yet solved to be able to get automatic Expo generation to be just actually automatic exploit generation rather than I know there's a bug on this line and is this type of bug why don't you just figure out the sled for me did you be actually kind of knew about Lang sec before there was a term for it so he realized that the parser that was Network facing would be the attack for

the attack vector and so he actually wrote that to be in a separate process that uses a very simple flat file format to communicate with like the mail routing and all the other what what not and so the parser is highly isolated which also makes it really easy for us to analyze we just analyze that part with having to worry about all the mail stuff so we did is we took that parser we ran it through CLE which is a symbolic execution engine that targets the lvm intermediate representation and we kind of gave it like timestamps like alright we run it for 30 seconds and one minute or whatnot and we just wanted to measure kind of the code coverage and

also we ran it for a while until the SMT solvers started failing because the constraints were getting too difficult to solve and we measure some running time we then took that same parser we implement it basically line for lime and crema and then we redid the same analysis to see all right if clean knows that the program is being run and it's going to be bounded it might be able to make more kind of assumptions and some of those constraints might be easier so you'll see the red dots are the number of states run and then the blue dots are the restricted ones in crema and so this is based on the length a symbolic length

of a string and a certain data structure and so as you go from you know like four five characters up to nine characters you go from just under a thousand to 7,000 so you get some pretty high growth in the number of states that has to visit and for each one of those states it actually has to go and create all these constraints send them off the SMT solver which is MP complete and then it has to wait a long time and eventually actually run out of memory in crash restrictive paths 45 is a little bit more manageable than 7331 you can also see this as a line graph basically the number of paths that had to explore and

menaces time bounded so after 10 seconds we basically quit the program to see how many states had kind of identified to be traversed and you'll see that it grows much faster for the normal versus bounded and then the last one you'll see here just the instruction coverage it covers a lot more of the program right off the bat there are some weird things about how this instruction coverage is measured the program hello world if you run it in CLE until pleats it will only say about sixty percent just because there's so many strange weird things in printf that require a string of a certain length or certain kind of quantifiers and controls and so the reason is capped it's mostly

the fact that it's just running into these library functions that it just can't explore because there might be some previous constraint all right that brings us to send mail so we're talking a lot email a lot I guess so most you guys know marked out kind of like a genius he found this bug actually in 2003 the in send mail so there's a very simple parser just to make sure that your email address that had matching parenthesis and matching angle brackets and they work nested or kind of confused and to make sure the email address is valid so basically took an input email address and then would output one with closed parenthesis if it needed some it

reserves space in the output buffer to make sure there's no overflows actually reserved extra space for those closed parenthesis and since then allowed nesting doll recovered too unfortunately he found that a pointer they were using rather than a length or using pointers arithmetic they found that it was failed to decrement and then it caused an overflow and so this basically got a remote code execution on send mail however then used this as basically a verification / automatic exploit generation problem is how could we have found this bug automatically and so that was kind of an open challenge from Homer and then in 2012 Julian basically showed how you would use an smt solver to find

that specific bug the only issue is is the analyst who was basically writing that verification question had to know about what the bug was going to look like because if you look at the source code it's just a while loop and you're not really sure that if it's entering through the loop Worf is waiting for some time condition or what and so it's very hard to generically see the badness on this unbounded loop there's a while loop if the programmer had gone a little bit further and maybe put in a for loop or for each loop to kind of loop through that input buffer then the the verification problem have been a lot easier because it would have detected

that it was looping through and then was looping past the end of the array and so this is kind of another example of something we're not necessarily the crema language itself but that idea of forcing the programmer upfront to really kind of figure out what its intent is his or her intent is and to implement that is it clearly as possible makes analysis and verification much easier and by basically making it very very difficult to put in these vague and ambiguous terms you're going to get very few hard to analyze problems how can I help you so basically we would allow you can limit the bounds the loop so that means even if someone did find this

exploit they'd be bounded to how many you know Luke's basically it had left through this parsing function programming verification tools would be able to text the program was outside its bounds you'd have a reference monitor that would be more powerful and it can actually recognize some of this overflow conditions and then the programmers and 10 is more naturally expressed as I talked about a while loop is kind of a catch-all to loop but it's kind of very difficult you see while loops do while 0 all the time and so you have that on one scale which basically is to wrap up some of your kind of see scope and then you have while one break in some other

programs and so then this is a perfect use case I mean basically this parser that on all circumstances should terminate you don't want to have an email address that will run forever trying to figure out where it should go so crema is useful reducing the length of rope programmers can hang themselves with even if you do implement a bug and someone just find a way to exploit that they're kind of naturally capped at whatever running time left so you think back to the tick-tock crocodile a crocodile that can only run fifteen hundred paces or whatever it is is a lot less scary than one that can kind of run forever a computationally bounded attacker is a much weaker attacker yes

so yes it will you so basically you are writing a so a sorting loop right you're going to go through you know a maximum of saying you know whatever the asymptotic running time is to maybe sort some input and so you're not necessarily saying this is the bound you just need to be able to express the code in such a way that say maybe reads through a string and looks for certain characters that's going to run I mean it so we're assuming finite input right so so so you can think of the halting problem right is trying to figure out of a program will terminate on a given input and you'll be able to essentially have that

finite input a priori criminal doesn't count how long the input is that was like the formal model that was kind of just for the math but what we'll do is it's basically it's very hard to hopefully impossible to represent a program that will be able to go through beyond the length of that input and so if you have a program that accepts input and you say yeah wait until the null terminator and you never send an adult Terminator crema will run forever in that regard because you're sending it essentially an infinite loop or infinite input but once it has everything read in and you can also think about this is fundamentally you could put in some kind

of symbolic variable for that length of input or that input at some point and then you could basically require them to put all their input in a priori kind of is like say command line arguments versus waiting and then you can do you know finiteness checks and then you can insert that in in a more concrete value so you're basically replacing that symbolic sighs with a concrete sighs once you get it and so counting the length of the string it doesn't necessarily mean how long it is it has to be finite and that you can't represent in crema a unbounded loop on say an input of any size and so the counting doesn't necessarily matter

unless you're doing analysis it more matters that you can't represent a program that will be able to take one input and then possibly run forever you just can't represent a program that does that because all the programs are using what's called wall for recursion and are halting there are some programs that would terminate that are not Walter recursion they can't be basically proven to be terminated and so crema can't actually represent those programs so there is kind of a some class of some problems that would terminate and could be sub to her and complete but because our recognizer can't recognize them as such they're explicitly kind of failsafe and so in a sense like that where you

might have some of these edge cases where accounting might be a challenge that would probably be a system an example of one of these outside of wealth or recursion problems that it would just kind of failsafe and just not recognize yes you have to give it a finite input yes and so that's why is the Apache yeah the program has to know how long it is yes all right so it's open source Thank You DARPA all the code examples documentation is up on crema lang org we hope you check it out we want you to hack on it submit patches start using it give us feedback right now we know it's very limited and the

standard library is quite shaky in the sense that just doesn't let you do as much as a Python does but we'd really like to K hey I will want to use it in this kind of project could you start doing some stuff more and say maybe more network parsing or whatnot and then hopefully by using crema your software will be magically easier to analyze and safer when I was at RSA I think I counted magic in vendor pitches maybe four or five times that this vendor appliance magically makes you safer so with that are there any questions feel free to reach us out on twitter if you have any questions or if you have any questions now or I'll be

around throughout the week so depends on the complexity of your match right so a regular expression is a very kind of constrained input language and so that right there would be very easy to put in to something like this and so you'd be able to submit that but much more complicated so kind of beyond so context-sensitive or you even have a higher complexity than that would not be because representing and being able to take in these complex data formats and being able to recognize them with us have to make it so think about recognizing PDF where you have fields they can point to other fields they can point all the way around in a circle if

you wanted to match on that that parser is going to have to go through and it's going to keep going around and around and around and so that will make your whole program get to the point where it's not going to be some tutoring lead I question first and come in our context support for functional programming functional programming style the context is we're developing a domain-specific language support a variety of agent-based modeling so we have scheduling lu handles when things execute agents do generally finite things within each step and we're creating a domain-specific language to specify what the agent student with a capable of and it turns out for application we have lots of things that

look like transducers we want to use functional programming style is a compact sufficiently expressive way to describe what they're what they're going to do and so I like everything conceptually about what you're doing I would like to be sold that crema would be a useful tool for us to plug into our Java gala sure back ok so functional language actually we're working on another effort to make basically crema more specific so you can actually say this function is Turing complete and this one is not and in how you actually verify software that's kind of mixed so when Nick did it scl for which is a formally verified microkernel they basically manually went in and categorized all the functions of their

kernel and said these ones are turning complete these owns or not one other ways we're thinking about representing is actually using continuation enclosure which is a very common formal methods and so we're actually working towards integrating more and more formal or functional paradigms in their first class functions etc so that's definitely something that I'm a functional programmer by myself you know typically and so that's something that I like to see as well thanks sure so the source code for crema itself is C++ which is just kind of a native llvm API and in it when you compile it you get crema CC which is essentially uses vary some more argument to GCC you can give it a crema

file it will either output a el file or l ll file for the lov mir or it will output just a flat-out a dot out type binary sure yep so that was one of our so you know when you go through and you pitch DARPA program they ask you to go through and find all the weaknesses if you can find some way to basically inject ir or inject the kind of you know at that level then you'd be able to bypass it right and so what darp is interested in is actually coupling this with sub Turing environments so imagine FPGA that also kind of knows about that and so that way even if you're able to

find some issue in the optimizer or find some issue where you can inject raw intermediate representation code into the JIT you'd be able to still be bound so they're looking at FPGAs they're looking at kind of restricted computational environments that's actually what we're talking to with some folks at Intel about how you make a see p mode so my usual background is really low level stuff so figuring out ways for the x86 architecture to do things that it shouldn't normally do and so we found a way to basically emulate a forward only execution model and so we think if we couple that you basically set a bit and some elf header vases saying this program should provably terminate and

then you'd be able to use cpu to basically prevent that breakout yes very good question that's definitely a identified weakness yeah so this would not be any CPU modifications this would just be yeah so one of the other work I did was called hairs it takes allows you to take a binary fully encrypted with AES and then run it at native speeds with the key never in memory and the decryption never the atribute instructions never reviewable even to a compromised OS kernel and so that was basically fully encrypted execution but done with no cpu modifications that was all done in software and so using that same type of capability to be able to do that for this so be basically a Linux

patch or maybe a thin hypervisor or whatnot that basically allows you to provide that without having to go out and buy all new hardware that's that's what I like doing is figuring out ways to like back port security to get it for legacy stuff

so moving forwards we're looking at the hammer harsha generator on my Meredith Patterson so we're actually working on a joint effort with them Hubble proposed effort at least to both formally analyze hammer to make sure there's no implementation flaws in that and then embed that right into the language so that when you're reading an input you're going to give it basically a hammer parsed generator definition and it will generate the code right then and there so you will only be able to formally specify your inputs all right thank you [Applause]