So I have the pleasure to introduce to you the speaker, the invited speaker of this session, so Karthik Bhagavan. So Karthik graduated from IT in New Delhi, if I saw this correctly, and then he did his PhD at the University of Pennsylvania, where he learned about programming languages, if I noticed this right. And then he went to industry at some point to Microsoft Research in Cambridge and got interested into cryptography. So his research is at the frontier between programming languages and cryptography. He got 2016 an award, so he's in France now, so I didn't mention that. So he moved to France probably as a good step, a good intuition in view of what happens nowadays in UK. So he's happy to be in France with India. And since 2009, I think, and leading the project Prosecco at INRIA, he's heading this project, and got 2016 an award as a young scientist of INRIA and the Academy of Sciences in France. So please, Karthik. Well, thank you for the kind introduction. So the very first conference I attended was FSTTCS, so it gives me great joy to come back here. And I wish there were more students like what I was then in the audience, but it'll still do. So today I'm gonna speak about a little bit of the work we've been doing in my group. And since it's Friday afternoon and you've all heard a lot of talks, I'm going to focus more on problems and solutions. So I'll show you what are the kinds of things we're trying to solve. I'll tell you a little bit about how we're trying to solve them, but maybe you'll have better ideas on how to solve them. Yourself, so these are problems that are very much still open. All right, so what do I mean by real world cryptography? So we're all using this stuff, okay? So you use WhatsApp, I guess. You use Skype. Underneath Skype and WhatsApp, there's actually a protocol. Well, if you use private conversations, which is going to give you end-to-end encrypted messaging. And this protocol is, well, for want of a better name called a signal protocol. Okay, it's a very fancy protocol. It tries to protect your conversations even if your device is stolen by somebody, they should not be able to read older messages. If they steal the device and give it back to you without you knowing it, they should not be able to read future messages. So they try to achieve lots of really fine-grained guarantees and they do this by using very novel constructions. So it's a very new protocol, but it's already ubiquitous. So WhatsApp, Skype, everybody uses it. A second example, which again is kind of invisible to us, but it's actually happening all over the place, is machine learning, of course, right? And a lot of people are now concerned that machine learning algorithms are not privacy-preserving, right?  They may have learned things about us that even we didn't know about ourselves. So there's a new field, which is getting growing a lot for called privacy-preserving machine learning and this involves a lot of cryptography. In fact, very modern kind of fancy cryptography. This is not working, so I'm going to stand here. Like secure multi-party computation. So just to give you an idea, so the model owner, like Google, owns a model, they don't want to show you the model. You have the data, you don't want to give Google the data and in between there's some cloud server, you don't want to give the cloud server anything. So you all want to hide things from each other but still do some fancy machine learning stuff. How do you do this? And there are protocols to do this. But these are still, both the protocols I've shown you are kind of fairly new, evolving, these are open, people don't really know how to think about them. So let's switch back to a very classic old protocol that we've all been using now for 15, 20 years and it's a backbone of the web. This is a protocol called TLS or transport layer security. If you go to your bank or whatever on Chrome or Firefox, you'll see this little green thing or a lock or whatever that will tell you that you have a secure connection with your server, with your bank or Gmail or whatever. In that case, this secure channel is provided to you by TLS. And this is a 20, 25 year old protocol. It should be like a very, very standard solved problem and there should be no problems left in this. Is that the case? Unfortunately not. So here's a selection. It's not a complete, it's a selection of attacks that came up on the TLS protocol, not too long ago, between 2011 and 2016. I haven't updated the slide. If I did it, it would go to another page if I continue updating it for the last three years. So there's a ton of attacks. The ones in red are the ones my team found. So we are kind of very familiar with this literature on these attacks. So this is a very well understood notion. I am going to my bank. I don't want my data to be revealed to the adversary and adversaries, anybody who's not me or my bank, we should be able to solve this problem. It's a classic cryptographic problem. So what goes wrong with things like TLS? And this is not just TLS. Every cryptographic system that is successful has attacks on it. And why is it so hard to get these things right? Well, there's three layers of things that typically go wrong. And for example, at the heart of your system is cryptography. And the cryptographic algorithm you are using, or the cryptographic scheme or construction you're choosing, may be weak. It may have some weakness in it that maybe cryptographers knew about, but you didn't know about, or maybe even they didn't know about, and suddenly becomes known, and then suddenly the scheme and the protocol collapse. That's case one. And this has happened for many protocols, and many algorithms at this point, and there's a brief list up there. A second example is, well, okay, the crypto is all fine, but the way we put it together to make this protocol where the client is gonna communicate with the server, the server is gonna do something, and so on, that protocol might have a design flaw in it. This is actually a rare error because people have been designing these protocols for 40 years now. So even before we had TLS, people have been designing these kinds of protocols, you understand how to design them, but there are still flaws in them because they're hard to get right. The compositions of these things, very easy to get them wrong. And the third kind of problem is actually the most ubiquitous one, the stupidest one, shall we say, but actually the hardest to get rid of, which is implementation bugs. You have done amazing crypto.  And often we have found in the kinds of research you've done is that the system breaks down due to a combination of all three of these.  And maybe we'll see an example or two of this kind of thing in the talk. So what shall we do? Well, we should try to remove these kinds of problems, but before doing that, because you're not so familiar with these things, let's actually take a look at some examples of what I'm talking about here. So some example attacks, okay? So here's the most simple core protocol that is taught in Crypto 101, which is the Diffie-Hellman Key Exchange. It's at the heart of IPsec, SSH, TLS, Signal, whatever you think about. Every protocol, every cryptographic protocol uses this at its heart. The idea is that there is A, let's call it the client, there's B, let's call it the server. They're going to communicate with each other, and at the end of the communication, they're both going to have a shared key K, and this key K is known only to A and B so that they can now use that to encrypt messages to each other without anybody else being able to see this. Okay, and so to do this in this protocol, A sends G to the power X modulo some large prime P, B sends G to the power Y modulo some large prime P, they both compute G to the power X, Y, and there is a nice assumption called the Diffie-Hellman assumption that tells us that the resulting key will be known only to A and B. Lying, of course, because in this case, there is no authentication, so there's a well-known attack on this protocol that I showed you, it's called the man in the middle attack on anonymous Diffie-Hellman, if you want the name for it, and the basic idea is the following. So A was sending the G to the X to B, right, but there's a network attacker, there's somebody on the network who intercepts this message, changes X to X prime and sends G to the X prime to B. Similarly, when the message comes back, G to the Y, it changes G to the Y to G to the Y prime and sends it to A, and at the end of it, both A and B think, ah, okay, we've connected, we've got our keys, but in fact, the attacker knows both the keys on both sides, so he's a, what they call a man in the middle, a person in the middle, who has completely taken over or hijacked this connection, and that's because A did never had to prove that its own identity never had to authenticate itself, and B never had to authenticate itself either, so this protocol was destined to be broken by a network attacker, an active network attacker would break this protocol, but there's a fix, there's a classic construction called Sigma, where Sigma stands for signatures, Ma stands for Mac, so Sigma, where you add a signature, a digital signature, and you add a Mac, and you need to add both, actually, if you add only one of them it actually, again, there are many other attacks that have appeared, so it took them a long time to figure this out, but finally, the cryptographers came to an agreement that what you needed to secure a Diffie-Hellman-like protocol is something like this, where you have a way of authenticating both A and B to each other, so they came up with this protocol, the details not so important unless you're interested in cryptography, and the security of that protocol basically relies completely on this one assumption, the Diffie-Hellman assumption, and let's look at it in a little bit more detail, so the key that you're going to be agreeing on is G to the power X, Y, mod P, where X and Y are two random numbers that have been generated between zero and P, P is some large prime, let's say it's 2048-bit prime, again generated as a large prime that has been generated, and everybody knows P, but X is known only to A and Y is known only to B, so the Diffie-Hellman assumption, the hardness of the Diffie-Hellman problem is basically the idea that if the attacker does not know X and does not know Y, then the attacker cannot compute G to the power X, Y, mod P, just given G to the X and G to the Y, so by looking at what's happening in the protocol, he cannot get the final key, and there are various many versions of this assumption that are written in different ways with different kinds of probabilistic assumptions made on them and so on, but this is more or less a high-level idea. Now, if I say that I've got the Diffie-Hellman assumption, I'm going to use my protocol that uses Diffie-Hellman, now you're going to ask next is well, yeah, but why is this problem hard? At what point does it become hard, and until what point is it easy? And in all things cryptography, you will find that things that are hard today will be easy tomorrow because the attacker's capability grows as our own computational capability grows, okay? So there is never a fixed thing, so today you're encrypting something with 2048 bit Diffie-Hellman, it does not mean that that is going to remain secure forever in 23 years from now, that 2048 bit prime might be very easy to break. So in particular, there are few groups around the world who are always going for the world record in breaking the discrete log problem, which is essentially breaking Diffie-Hellman. So in 2005, there was a record which they broke a 430 bit prime, which means if you give them G to the X mod P, they could give you X, but they could compute the discrete log for a 430 bit P, and this number has grown consistently, okay? Now we know for certain that we can do 768 bit primes, it is believed that the NSA can do 1024 bit primes, but we don't know, but maybe they can. Maybe bigger, we don't know. All right, so that gives us a bound. So it says that don't use primes up to that 1024 bits, otherwise you're screwed, right? So let's say 2048 seems safe, so that's why I put 2048 on the previous slide. But we have to be aware that there is this weakness if you use a weak P, yeah? So how do protocols get around this? So there are some weak P's and there are some strong P's, right? And the way they get around this is by doing negotiation, right? So 20 years ago when IPsec was first started to be deployed, they used primes which are 512 bit and 768 bits. TLS also had a 512 bit prime for export use, which means everything but the US was allowed to use 512 bits and people in the US were allowed to use 1024 bits, okay?  But normally we never want to use them because as I said, 512 bit is too weak, okay? So every protocol out there, SSH, IPsec, TLS, whatever you use has a negotiation phase. In the beginning Alice is going to say to Bob, hey Bob, I support these two groups, one of them has 2000 bits, one of them has 500 bits. Which one do you support? So Bob looks at it and says here, I support 2048 bit group, so let me pick the good one. I'll pick the best one and we will both work on the best common group that we have between each other. This is a bit simplistic because there could be many different groups for 2000 bits. So it might say, I support these 3000 bit groups, you support those two, okay, let's pick one that we both support and we'll continue. And this is called negotiation. All protocols need to have this, otherwise you will never be able to communicate between a Microsoft device and an Apple device for example. Because they support different things, they have to find something in common, okay? And in this case, nobody really wants them to ever choose the 512 bit one and they will not normally because now if you take Google Chrome and you connect to Gmail, they both will support the strongest one, they will choose the strongest one and they're done. So normally this means that everything should be safe, right, except not. Because there is a man in the middle attack, remember the one anonymous defilement, the same kind which works on that kind of negotiation protocol, it's called a downgrade attack and the idea is the ideas are following. So there is a network attacker as before who's looking for messages that you're sending to your bank. So your browser sends to the bank and says I support these two groups, a strong group and a weak group. The attacker deletes the weak group and just, sorry, deletes the strong group and just lets the weak group go through. So the server looks at this and says, oh, this must be a really old client, maybe a printer or something. Okay, I don't care, if he wants a weak group, I'll give him the weak group. So the server says, okay, let's do the weak group. Now on the way back, the attacker just lets the weak group go back to the client and client looks at it and says, oh, this must be a really old server, maybe a printer or something and I don't care. So, okay, if he wants to do a weak group, we'll do a weak group. And they both downgrade themselves to the weakest group because the attacker tampered with the message and they continue with the whole protocol. The whole protocol is done with 512 bit security which the attacker knows how to break, okay? That was the basic idea behind this attack called the log jam attack that I and many of our colleagues found in 2015. For that, we had to use a specific crypto attack on 512 bit groups, for which we did a lot of crypto analysis with a group in Loria in France. Then we had to figure out how to get the protocol to downgrade which we did in there. Then we kind of found all kinds of groups around the world that people were using and showed that a huge number of these groups were vulnerable to this which is done in the US. And so this attack was actually practical against a significant chunk of the internet. You could break the connections to them by using this attack. And that's not the only one. These kinds of downgrade attacks where you support something strong and you support something weak for legacy backwards compatibility reasons happen all the time. So there are like four examples up there. You can get the attacker can basically force you to use the weakest possible option that you have, okay? And this basically makes it very problematic to fix these attacks. So if you upgrade your software the any software that you upgrade. So you had an old version and now you're getting a new version. The new version is never going to delete the old version. It's going to put the new version in addition to the old one. So now you always have this downgrade possibility that the attacker can force you to use the old version when you did not want to use the old version. So the only fix really for protocols like TLS and for other protocols like this is to really get rid of everything old. Make sure that anything which is known to be broken does not exist in the software anymore, okay? This is notoriously hard because things hide somewhere in the software. You think they're gone but they're not gone. OpenSSL is hundreds and hundreds of thousands of lines long. Chrome is a million lines long. You can't be sure that MD5 has been removed from everywhere and probably it is there somewhere because someone does have an old printer that they do want to connect to and they can't get rid of it. And the worst part of it is that even if you manage to get rid of all this crypto problems and fix all your downgrade issues you may still have implementation bugs. So let's take a look at that. So in TLS 1.2 there were two kinds of handshakes that everybody was using. A handshake is like a protocol for setting up the key like the one we saw for Diffie-Hellman, right? So one of them was not a Diffie-Hellman one. It's called RSA. The details are not so important but it basically had four messages and at the end of it you had a key, okay? And the flow of messages was something like the one I'm showing on the right. So there was a client hello, server hello, server certificate, server hello, blah, blah, blah. The sequence of messages going between the client and the server, at the end of it both of them have a good key. It also supported a Diffie-Hellman mode like the one I showed you which also had a similar flow of things which has slightly different cryptographic constructions but at the end of it again, you have a good key. If you just look at the messages that were on the wire there was only one difference between those two which is the one which is circled in green which is that in the Diffie-Hellman mode there was one extra message, okay? Which was a G to the Y that the server had to send back to the client. There's one extra message called the server key exchange otherwise all the messages more or less were the same which means that if you wanted to write an implementation of this and you wanted to write parsers for each message and the state machine for each message and what to do when you get this message or that message or what error to send and so on which is all this code that you had to write in protocols you really want to share all the code as much as possible between those two modes except for that one message which is extra here, right? So you want to compose the state machines that let's think of them as state machines, right? These two state machines for these two protocols and you want to compose them in a way that you share as much as you can. So this is what I would say is the composite state machine for those two the one in the middle, the one on the left is RSA the one in the middle is Diffie-Hellman and one on the right is a composite state machine it has one branch.  Now this is just looking at the message flow, yeah? Inside the messages there is very different data going on here and we still have to do some interesting trypto and so on but just looking at the overall message flow what the state machine looks like and this is for just the two modes that we have looked here in reality TLS actually has many other modes it has this thing called resumption it has some other kinds of PSK modes and so on so if you take all the modes that are commonly used on the web the state machine looks a little bit like that on the right so it's a bit more complex it may have a few more branches but still more or less something that you could code up in almost any of the verification tools I can think of so that's I would say the state machine for TLS as it's used on the web, right? So it covers most of the features but the state machine I've shown you there is actually something I've invented it's actually not on the spec nobody really agrees on what the state machine should be it's something you can infer by reading the spec so it's a good question to ask is this what real implementations do? I mean this is my guess of what they should do but is this what they do? So you can take that as a spec and test existing implementations or in this case fuzz existing implementations to see if they follow that state machine and we found when we did this exercise in 2015, 2016 that a lot of implementations of this protocol even in your browsers and mainstream servers mainstream browsers did not follow the nice state machine structure I had before on the right is OpenSSL one of the most important implementations of TLS which is used on almost all web servers websites everywhere and it had these extra edges in the state machine an extra edge is when I expect you to not accept this message but you're accepting this message or I expect you to accept this message but for some reason you're not accepting this message that would be one less edge so what is some cases always the extra edges? Are you accepting something you should not accept? So the ones in green are the extra edges that are accepted by the server the ones in red are the extra edges that are accepted by the client in the OpenSSL then if you go look in Java because Java has a TLS implementation so if you ever do a HTTP connection from your Java program to PayPal or eBay or Amazon or whatever which a lot of people do because this is what Java APIs are for then you'll be using the Java TLS stack and the Java TLS stack has a ton more extra one pretty much you can go from any state to any state so it's not a state machine anymore it's just a fully connected graph so they have done this pretty bad implementation let's say where I just allow you to send any message after any message and the hope is their hope is that well doesn't matter at the end of the protocol if we screwed up then the keys will be different and so nothing's bad is going to happen and while the protocol is going on let's just take any sequence of messages we'll try to process it the best we can if something goes wrong we'll throw an error it's not a big deal so this actually can be traced back to this notion that came up in the early days of the internet where I think it's called Postals Principle which is it says be strict in what you send but be liberal in what you accept and this was at the heart of the interoperability that drove the internet which meant that if Microsoft was doing something crazy with that stack or Cisco was doing something crazy with that stack they would still try to accept some weirdness from the other side because they don't know what exactly you're doing so you have one extra bit okay I'll try to figure it out what you're doing so they would be willing to accept more crazy stuff from the other guy but when they were sending they would be trying to send straight up stuff so that could be one reason why these guys are willing to accept so many extra edges which should not be accepted but here's the question is this actually a bug or is it just a badly designed thing or maybe my spec was wrong well of course it's a bug and it's a bug which is exploitable so say you're using PayPal's Java SDK which a lot of merchants use online so if you click on pay with PayPal or something like that then it's going to use this Java SDK to do this payment with PayPal so the Java SDK your merchant side is connecting to PayPal your attacker is in the middle he wants to intercept this message but pretending to be PayPal of course he's not PayPal so he doesn't know PayPal certificate the first thing he does is when the client sends a hello he stops the message and he sends back PayPal certificate PayPal certificate everybody knows he can do this, no problem the next message after that is this thing called the server key exchange message that he's supposed to actually sign with PayPal's private key but he doesn't know PayPal's private key so he can't do this so what's he going to do but the Java state machine allows him to skip messages so he's going to just skip this message so let's see then he's supposed to send this message called a server hello done but if he does this then the client is going to start sending more messages and he doesn't know how to process them so he's going to skip the next message but once you skip the next message the client is still waiting which means you have effectively skipped the next four messages and now you're in the next message that the server is supposed to send called a CCS but if you send the server CCS message it means that everything from now on will have to be encrypted but we don't have an encryption key we have done nothing we didn't do any crypto whatsoever so there is no key we have not done nothing so far we just skipped everything so what are we going to do now so what this guy does is he says well let me try the same trick he's going to skip that message too now there is this last message which is the finished message which means that the protocol is finished if you don't send that message everybody is just waiting nothing has happened everybody is just hanging on the phone so you have to send that last message but that last message requires you to send a MAC and the MAC requires a key and the key was the key we were supposed to have agreed in this protocol but we have done nothing in this protocol we haven't agreed on a key but Java has this nice feature that Java is a type safe language which means that of course it has a slot for the key and of course the slot for the key is initialized to all zeros so maybe you can use all zeros as a key and try to send this message and if you do it will accept it and at this point we have bypassed the whole protocol in fact we didn't even turn on encryption so the client will start sending messages in the clear to PayPal thinking it's fully connected to PayPal but in fact it never even touched PayPal what's worse here is that at this point if you try to if the client tries to ask Java hey Java tell me what kind of connection do you have it will say oh don't worry we have 5,000 bit security we have the here's PayPal certificate which has this 4,000 bit certificate everything is like the best quality crypto that you can see but actually all the crypto was bypassed because of the state machine bugs so this is a particularly bad case where the protocol the implementation bug in the protocol which is a state machine bug allowed you to completely bypass the full protocol completely but there are many other cases which are more subtle than this where you bypass one message then you have to do some crypto trick then you bypass another message and so on so even if you find a tiny little one bug somewhere in an implementation you should never assume that oh this can't really be exploited this will lead to an error because you don't know there could be some combination of things that will allow you to break this so the summary of that stupid attack on the previous slide was that if you were using Java to do anything secure before 2015 you shouldn't have bothered you were pretty much completely at the mercy of the attacker and this is true between 1997 and 2005 for 16 years whatever something around that there was this bug which nobody noticed so let's get back so we saw crypto weaknesses for logjam we saw protocol flaws like downgrade attacks we saw implementation bugs like that silly thing in Java so this is just a sample so how do we be sure that the WhatsApp thing that I'm using on my phone or the TLS thing I'm using to have interacted with my bank is actually correct is actually secure so this is where we argue that you can't do this it's too complicated you can't do this just by staring at the documents you need formal verification so formal verb methods are the only method I know for getting any kind of confidence in complex systems like these and this is a very good and impactful area for you to apply your techniques as well if you have some new techniques that you want to try out because clearly if you break something here it breaks the security of something important so the impact is usually pretty straightforward so in particular in my group we've been looking at doing symbolic analysis and I'll show you an example to find attacks we took cryptographic proofs of security using tools like CryptoVeref and F-star we also developed CryptoProtocol software verified software using F-star but there are other groups who are using other tools like Coq, CryptoVST, Tamarin and VisaCrypt and so on and all of these tools are coming to a level of maturity that many of you should be able to use them to do effective things so let's take an example of what we can do with these kinds of tools so the first one is going to be how do we verify something like TLS that it doesn't have some of the kind of downgrade attacks that we saw before and in particular let's look at TLS 1.3 so last year, 2018 the new version of TLS 1.3 was released to big fanfare actually there's a lot of news articles and so on and that is because it took about four years of effort to standardize this new protocol 28 drafts, 12 meetings lots and lots of people were involved and primarily it took much longer than they expected because as they were developing this protocol more and more of the kinds of attacks that I showed you before started appearing in the old version of the protocol and then they realized that they had to throw away completely TLS 1.2 and start from scratch if they have to avoid these protocols these bugs in the future but what's more this time they did an experiment they invited academic security researchers including us but anybody who was interested to come and help them analyze the protocol as it was being developed the protocol, its implementations is cryptography and so on so even before the standard was finally published there were like 10 to 12 papers in major conferences analyzing the protocol saying this is good this is not good and so on so this really was a very symbiotic relationship between the researchers and the standardization body and I was involved in some of this work as well so what is new with this protocol? well the first thing they did and good thing they did is to throw away all the bad crypto so they killed all the bad crypto and they added new downgrade protection mechanisms which should actually be designed to make the protocol stronger so that was a good thing they did the bad thing they did is they tried to make it faster so they added this new mode called 0RTT which really allows you to do connections really very fast and it's a bit dodgy it's not really something I would recommend people use but they have a new mode called 1RTT which is already faster than the previous protocol and it's actually very good and that's the mode that I would recommend everybody use the third thing they did was they completely changed the way TLS works with its applications so that the composition of various modes of TLS and of TLS and its applications becomes cleaner and this we don't know whether it will actually have an impact in the future we have to see as new applications comes up whether or not this is going to make a big difference but all of this put together meant that this is a completely new protocol which looks nothing like what the previous protocol looked like so if you want to write the whole protocol out and if I was writing in my papers this is kind of what the protocol would look like it's too big, I'm not going to explain this here but it's basically, this is the 1RTT handshake which is the main key exchange kind of component it has 12 messages and three flights and 16 derived keys and then you can do messages, messaging so you have to like derive 16 keys before you can start sending messages and in addition to this of course you also have other modes which are faster but one important thing to remember is that TLS 1.3 was released last year TLS 1.2 was released in 2008 so this took 10 years for the next version to come out and TLS 1.2 only became ubiquitous in the last three or four years so it takes a long time for new versions to completely dominate the landscape so we expect that in another five years TLS 1.3 will be everywhere but until those five years are done you're going to have TLS 1.2 and 1.3 running side by side okay so now we have to worry about this because you have an old version and a new version which means possibly downgrade so we have to think whether or not there could be downgrade attacks from 1.3 to 1.2 so let's ask this question I showed you, I flashed you a protocol in the previous slide now is this protocol provably secure? for 1.2 I told you it is not provably secure there are lots and lots of attacks 1.3 is it provably secure? we can ask this question and we can try to formalize this so remember this was what we started off with this is my connection to my bank I have some very standard security goals I want a secure channel I want there to be confidentiality on my password which I type and my bank account details and I want authentication I need to know that I'm talking to my bank my bank needs to know that it's talking to me so we want mutual authentication between ourselves okay but this is a classic secure channel so how do we formalize it? so this is not obviously the formal statement which will take several pages but this is roughly what every formal statement of the secure channel would say so first you have a model of the protocol so in this case we are saying that the client and the server A and B are both, one is a TLS client one is a TLS server you'll see what that means we want them to be honest so let's assume that we are talking about only an honest client and honest server which means that their own key material is secret the attacker does not know their key material but the attacker and then we have to define a threat model is in full control of the network so anything that goes on the network the attacker can read, write, modify, whatever furthermore, the attacker is in control of all other clients and all other servers so let's just focus on these two guys who we want to protect assume that everybody else in the world is corrupt okay, all the other clients and servers then the security girl is that if A sends a message M to B the attacker should still not able to learn this message M okay so if the whole world was using a crappy version of TLS but you and I are using a good version of TLS that is probably secure then it must be the case that our messages are still secure between us so that's like the definition of a secure channel now in order to make this more precise we have to say what is our execution model what is A running, what is B what is the definition of the attacker and there are several different ways of defining this broadly classifiable into two classes there's a symbolic methods and there are other computational methods in the symbolic methods we say that A is a high level program that uses, that basically manipulates terms and sends terms on the network where a term is a symbolic term called doll of yaw term or a medium shoulder term which abstracts around cryptography so an encryption is a constructor a decryption is a destructor whereas the computational model which is what the cryptographers use says that the A and B are actually probabilistic polynomial Turing machines and what they're doing is all their computations are over bit strings so the things that you're communicating are bit strings the things they're computing are bit strings converts similarly if you're only modeling the attacker in the symbolic model it's another high level program which is also at the same level as A and B and it has the same computational power as A and B whereas in the computational model it's also a PPT machine it's also allowed to only do manipulations on bit strings and there are some very strong ways in which we limit what it can do with cryptography so among the security goals if I'm trying to say that M is secret in the symbolic model I say that in all traces of the model M cannot be obtained by the adversary in the computational model I try to say that even a single bit of M will not be revealed to the adversary up to some probability P so in the computational model all the statements are probabilistic in the symbolic model they usually are probabilistic or trace based so for TLS 1.3 what does this mean? it means that what you're going to do is you're going to write down concrete models as high level programs let's say in the symbolic model or in the computational model of the client in the server and there are many different ways you can do this and here's just a sample we're going to use the applied by calculus which is a source language for this verification tool called proverif but you can use any of these other languages as well if you're depending on what kind of analysis you want to do then you're going to write down your threats by modeling the precise cryptographic assumptions of what the attacker can do and what he cannot do again this is simpler in the symbolic model in the computational model they're very well known ways of writing these as probabilistic equivalences and you can do that too and we have done that as well and finally you're going to write your security goals so let's do this exercise this is what TLS 1.3 server looks like in proverif it's the applied by calculus so there are inputs there are outputs you can generate fresh keys you can call cryptographic functions and you can trigger security events the details of this code is not so important these slides will be online so you can start at them later or you can actually start at the full model they should be much more informative and so in this case this is applied by calculus which is verifiable using proverif if you take the full model including TLS 1.3, 1.3 and 1.2 the full protocol you can model in about 500 lines of applied by so it's not a very big model actually it's one of the larger models you will write in these tools but it's not so huge then you have to write your assumptions about the crypto and that will take you about 400 lines if you are doing a computational proof this part, the writing the assumption is the most hard part so that will take you maybe thousands of lines but you can still do it it's still analyzable and finally you'll write your security goals in about a couple of hundred lines so in a thousand lines or something you have your full model of TLS and you can press the button on proverif and ask is this secure or not and proverif will give you some answers so before going into how we call proverif here's, I mean remember, recall that we have to define a threat model in proverif this is the threat model we'll have the attacker is a fully powerful network adversary you can do anything on the network and we're going to add this fact that the attacker is able to exploit downgrade attacks which means that we're going to have not just strong cryptographic algorithms but also weak cryptographic algorithms so the weak ones attacker can break but the strong ones he cannot break normally symbolic dollavio models don't do this but you need this if you want to truly look for downgrade attacks like the ones like the log jam attack we talked about before so we have this new kind of model and now we can start analyzing stuff so what kind of goals can we ask from proverif we can say can you prove that M is secret can you prove that M is authentic can you prove that it's forward secret which means that even if my keys are compromised later M will still be secret and so on so here's the simplest one this basically is asking whether this message which is sent on a particular connection to a particular server is will ever be known to the attacker so this is called a security query in proverif you can ask this about our TLS-13 model and proverif will immediately come back and say oh yes there is an attack the attacker can get this message if the server's private key is compromised but you say yeah yeah but you know I'm only considering honest servers so let's assume that the server's private keys cannot be compromised and last ask a second query proverif will come back again and say oh no this can still be broken if the authenticated encryption algorithm you used is weak if I say okay but I'm using TLS-13 there are no weak algorithms anymore so let's cut that out and then we'll find the next problem and the next problem and so on the next problem after this it finds is that the Diffie-Hellman algorithm might be weak and this in fact is a log-jam attack and this you can't eliminate so easily because TLS-1.2 does use weak Diffie-Hellman algorithms so if you have a TLS-1.3 server that also supports TLS-1.2 and that TLS-1.2 part of it supports a weak Diffie-Hellman group then you can do two hops of downgrades to get down to the bad Diffie-Hellman group and then you can break the connection so this is actually a real attack and so on and the final the strongest query to which Proverif-Alans are true is this one and if you look at this carefully it basically is listing all the conditions under which your connection is secure or put another way all the conditions you must satisfy before TLS-1.3 become secure it says for example if you read it out is that messages on a TLS-1.3 connection are honest and this is a security theorem it's proving for us in the symbolic model but it's proving as theorem here if as long as the connection does not use bad algorithms and as long as it does not use weak Diffie-Hellman groups in any protocol and that's kind of some of these assumptions but not obvious to the designers of TLS-1.3 either but this has now become an advisory for how you should deploy TLS-1.3 and I would argue that this kind of problem where you're finding attacks on the combination of TLS-1.3 and 1.2 where each of them has five modes each and each protocol has like 15 messages is impossible to do by hand you definitely need formal tools to do this and you will never be sure that you've found all the attacks unless you actually have a formal verification tool that can actually give you a positive result at the end of things so that was one piece of the puzzle there are other people who did crypto proofs some people who did proofs by hand some people who used tools to do this but there was a whole bunch of proofs that came up for TLS-1.3 which is what gave us enough confidence to say maybe this is ready for publication it doesn't mean that the protocol doesn't have bugs it just means that we have bashed at it as much as we can with the tools at our disposal and new attacks that will come out hopefully will uncover new problems not old problems so now I'm gonna change tracks a little bit so so far we've been talking about protocols TLS, blah, blah, blah attacks, downgrade, fixing this and stuff but like I said all of these things are in the end going to be dwarfed by the kinds of problems you can have when you implement them we already saw the state machine bugs that come up when you try to implement the protocol but let's assume that was just a stupid bug everybody knows how to implement the state machine you know how to do it you will do it correctly maybe you can verify that the state machine is correct and in fact we do these kinds of things as well but the hardest part of any crypto library of any protocol library is actually the crypto layer because the cryptography that you're gonna use actually is fairly fancy mathematics and that fancy mathematics is hard to implement correctly so what you want is also a verified crypto library you can't trust that the algorithm that you're using whether it's RSA or Diffie-Hellman whatever has been implemented correctly there are tons of bugs if you go to any crypto library people are like constantly finding bugs in this thing so this is a different project I'm going to speak about which is taking most of our time right now which is we are building this verified crypto library called Hackle Star we've already released one version a second version is going to be released next month and let's try to see what the problem is what is the problem we're trying to address here okay so how do people write crypto code the first thing you start off from is some kind of standard so the NIST in America or the IETF which is international or somebody else publishes a standard so this is a standard called Cha-Cha-20 Poly 1305 it's fairly recent 2015 it's a encryption algorithm and a MAC algorithm Cha-Cha-20 is encryption Poly 1305 is MAC and put together they give you a nice construction called AEAD which everybody wants to use so this is one of the more popular new encryption algorithms that has come up so if you look in the code if you look inside the standard you will find some pseudocode so there is some pseudocode there says this is what you should do this is the block encryption function this is it's kind of almost looks like Python but it's not quite it's kind of semi-formal pseudocode which tells you what the code should be doing and then you're supposed to take that and you're supposed to implement it and typically in C some people implement it directly in assembly and so on and if you look at the C code it looks more or less like what the pseudocode looked like so you can argue that there is not much that can go wrong between the spec and the code except maybe okay now you're doing some memory allocation so you could have a memory bug for sure you also the algorithm that is specified in the spec only says oh here's how you do encryption of one big block but in reality you never do encryption of a big block you do it like chunk by chunk by chunk so you have to figure out how to do that chunk by chunk encryption the standard will not help you with that so there are some more things that could go wrong because you did this wrong okay but on the whole there's not very deep things that can go wrong here okay so let's accept that okay so we could have introduced a buffer overflow or there could be a timing leak we'll talk a bit more about timing leaks later let's look at the other algorithm there it's poly one three of five which is a Mac algorithm actually that's the full spec of that Mac algorithm it's very very tiny you can describe the whole algorithm in about what 15 lines of Python okay it's very very tiny okay and this is what is usually used if you're using your phone on chrome on phone to connect to gmail they're using this algorithm and if you look deep inside that algorithm there is two lines there where it says a equals a plus m and it says a equals r times a modulo p this p that they're speaking about is actually a 130 bit prime there are other standards like this where it will be a 255 bit prime some others for the 521 bit prime they're specific prime so this is a 130 bit prime so the moment you look at that you realize that when you're doing this addition and you're doing this multiplication and this modulo operation you are not working on 32 bit numbers okay you're not working on numbers that are available in your programming language 130 bit numbers doesn't exist in any of our programming languages we use right now so this is actually a big num computation it's a computation on a number which is larger than what your platform provides you so how are you going to implement just those two lines that those two lines account for most of the complexity of the implementation of poly so if you look at it it basically breaks it down it says 130 bit number I'm going to represent it as 532 bit numbers actually you only need it four and a bit but you have to use five so it makes enough that you can use put 130 bits in it and now when you do addition you have to add it like two arrays like a big num addition of two arrays of 532 bit numbers you're going to add them and you're going to propagate carries you're going to do all kinds of management and so on so there's a lot more code that's a very much larger implementation than char char 20 and they can have lots and lots of bugs and people have found carry propagation bugs arithmetic bugs buffer overflows timing leaks all kinds of problems in this code which was not there in the other code so this is the kind of place where you can very easily find problems in your crypto software and to see why let's go back not just to crypto 101 but class two or class one or whatever when you first learn how to do multiplication right this is textbook multiplication of bits so this is how we do it we all do it for digits but okay for bits and remember you have to do this carry and you have to do this add and the add might have another carry and so on there's actually two carry bits that you have to carry around when you do this kind of multiplication and you don't need to know the details but in fact it turns out that you have to go back to class two when you do this kind of coding because that's exactly the kind of computation you are doing when you're multiplying 130 bit numbers or 256 bit numbers so if you're multiplying 256 bit numbers it's gonna look something like this you're gonna break it up into 64, 64, 64, 64 so there are four bits let's say four digits and then you're going to multiply them you're gonna have to carry along and you're gonna have to carry down and you're gonna add everything and so on the only special thing is this is modular multiplication so at the end you're going to take your seven limb or eight limb number and you're gonna have to reduce it back modulo p to come back to a four limb number and there are many algorithms for doing this and more and more fancy optimizations for doing this some of our instruction sets give you special instructions that help optimize some steps of this because it's so common that you would want to do this for any big num computation whether it's in numerical computations or crypto and this multiplication right here is a dominant cost of cryptography on all your devices just multiplication and typically multiplication of 256 bit numbers it used to be multiplication of 2000 bit numbers which is more serious but with elliptic curves now typically it's 256 bit numbers that you're multiplying and that's the dominant cost of crypto for all the protocols that you use okay because here you're doing n square 64 times 64 multiplications and that's kind of costly if you do Karatsuba you can do a little bit less and so on but it's more like this but let's worry more about the correctness of these things now you're gonna have these long intermediate arrays every number is an array so now you have to allocate these arrays deallocate these arrays make sure you copy them correctly and you have many many carry steps that you have to do all over the place to make sure that the numbers you're computing are correct right so what can go wrong you could have integer overflow which is very common which in some places will give you a trap and in other places is okay but it'll just give you the wrong result you could have buffer overflow and underflow of course you could have missing carry steps which is surprisingly a common bug that people do in this typically when they're optimizing their code or you could have a side channel attack so let's look at what a side channel attack in this case would be going back to the simple multiplication there so when you're multiplying like this one zero one one zero one zero one zero one zero you might observe that when you see a zero bit you really have to do nothing there's nothing going to be added because you can just shift and you can move on you can just ignore the steps where there is zero because there's really nothing happening and if you do that you cut down the computations you have to do by half which is nice so it's much faster fewer additions, fewer carries the negative is that if somebody is looking at how much time it took you to do that multiplication they now know how many zeros are there in the second argument and since the second argument is often a key a secret key knowing how many zeros are there will allow them to mount an attack that will soon reveal your entire private key so that is a timing side channel where the time taken by a computation is revealing things about your arguments and that revelation is enough to break the cryptographic algorithm that you're going to do okay so almost all the crypto code you are going to ever want to write is going to be constant time in the sense that you never want the running time of the algorithm to depend on any secret input so that's a very important criterion so okay so we talked about buffer overflows all these kinds of carry bugs and so on let's start how do we verify this code so the idea here that we're using is that well don't just go straight from the standard let's write a formal spec which is halfway between the standard and the code okay and then we will prove that the code that we are generating is correct with respect to the spec so it's functionally correct it's memory safe and it has no timing side channels that's what you want to prove and that's what we do with this language called fstar and we have built this library called hacklestar which I'm that paper is about it and stuff like that and the stock is not long enough for that but you can go look at it and ask me any questions you like it already supports a wide range of algorithms and we're growing this in which we prove memory safety, secret independence and functional correctness and the code that we generate from it is C code which is fairly portable we can also generate WebAssembly code and this code is currently used in Firefox in the wire guard VPN which is in the Linux kernel and in the Tezos blockchain and the concordium blockchains so it's already kind of fairly widely used so what makes this as a formal methods project which is actually verifying code what makes this actually take that last step towards impact is performance so when we try to get our code into Google into Firefox and stuff the first question they ask was how much slower is your code than the code that I already have my code may not be correct but it's fast but your code is correct but it's slow I'll probably stay with my incorrect but fast code and they gave us numbers like you can't be more than 5% slower because for Google 5% translates to millions of dollars on their data centers so that if you take 5% slower down unless they are so sure that their old code is buggy they will not change but what's nice is that if you're doing your verification technology in the right way and you're generating code which is C which is also verified then you can cross this gap so the code that we generated for Firefox was 20% faster than the previous unverified C code so it was a no-brainer for them to accept it and now we have jumped that by two times or three times even so we are much faster than what they ever used to have and in fact if you want to go all the way to really hand coded, assembly code that people write to get maximum performance out of these algorithms you can even do that so there is a project called Vail where they verify assembly code for arithmetic programs like the ones we're writing here and you can compose verified code from Huckle and verified code from Vail to get essentially the fastest crypto implementations that have ever been seen and that's in our paper called EverCrypt which will come out in Oakland this coming year so the end result of this is that if you go to if you open up Firefox, you go to Google and you go to the console you'll see there it's using X25519 and that's our code and not just that there's another five algorithms that they have taken from us and so all connections between you and Google is using verified crypto done by us it's not just us though there's a group in MIT who have this project called Fiat Crypto and they've delivered code to Chrome so even in Chrome there is one component of it which is using verified software of this kind okay, stepping back just as kind of quick summary I've told you about verified crypto, verified protocols but there's of course tons of interesting problems here you're working on verified messaging and there are many other groups working on this as well which is like WhatsApp but also group messaging and lots of open challenges there they've also been working on verifying privacy preserving machine learning algorithms with Prasad and this is again a huge area increasingly important area that we need more people to pay attention to and work on and all of this is under these two projects that I participate in one is called Circus and one is called Everest and I welcome you to go look at the web pages and see all the various kinds of things that people have been doing around verified software and verified crypto in these projects okay, conclusion but I hope I have given you a little bit of a flavor to convince you that formal methods are at this have reached the stage where we can be effective on real world crypto protocols but also have a real significant impact so it's an exciting time to be because all these tools have come to maturity we know how we can really have an impact but there's still lots of nice important and open problems left like we don't know how to do zero knowledge proofs you don't know how to do group messaging and so on and the other thing is that on the software verification side we have I think at this point in our development as a field cross the bridge where we no longer have to sacrifice performance for correctness we can make high performance in fact higher performance than existing code which is verified at least in this domain so it's again a domain that I would encourage you to look at again many many challenges everybody who's ever doing any blockchain related research is very wants verified code here and they don't have enough people doing machine learning of course and then there is this whole new field of post-quantum crypto which is untouched so there's like nice open areas where you can do lots of interesting work here alright so I'm going to conclude with this last slide which is to say that we are hiring and we are always hiring we are looking for excellent students and PSE students and postdocs so and visiting researchers so if you're interested in any of the topics related to anything that has spoken of today do get in touch thank you thank you very much for this very interesting talk so we have now some time for questions what about I mean protocols like what's up where you have multiple participants in the protocol so where you have possibly multiple attackers so how do these tools and these formalizations work with multiple attackers? we just submitted a paper on group messaging so there is this new effort at the ATF called messaging layer security but what the question pointed out was an important one which is that we are all we kind of understand what point-to-point security is but security for groups is a completely different beast because even stating the properties there is hard and especially when you have WhatsApp groups well WhatsApp groups go to 256 but there are messaging groups that go to 10,000 people but what is the security assumptions here? how do you kind of protect the group against one malicious participant or maybe n by 2 malicious participants is a completely new set of challenges so there are new protocols including the one in WhatsApp which can be analyzed with methods similar to what I said here except that they very quickly grow to very huge state spaces so almost anything that is based on symbolic model checking or something finitary will immediately fail in these group settings so you need something verification method that can really handle induction and recursion and so on to do this and F-star is one such method Hock is another method which would allow you to analyze these things but there are lots of interesting challenges Hi so sorry I think part of it you covered in the last part of your answer that is in F-star you indicated the kind of functionality that your verification engine would have I wanted to ask you about the underlying technologies from formal methods side but you said induction but then you said it is completely mechanized right so I in that talk the first part I was talking about Proverif and Proverif is completely mechanized it is a HON clause based solver now the one thing maybe I should have mentioned earlier in the talk is that the essential sort of verification problem we are tackling here which is with an unbounded attacker is undecidable, instantly undecidable actually so it's very easy to prove that it's undecidable which means that almost that all the verification tools you can consider here either are computing are doing very heavy approximations to get it into a bounded state or even or more commonly what they do is they give up on completeness so if they say yes it is secure, if they say no there is an attack but they may say maybe or I don't know and so Proverif is one of the latter ones it can say I don't know and then you have to use some tricks to kind of nudge it in one direction or the other and that's up to your ingenuity so most of the time for many of the classic protocols it will always give you a yes or no answer so it's very lots of heuristics in there so that part is completely mechanized if you want to do crypto proof like a true crypto proof with probabilistic polynomial tuning machines none of those tools are fully automated, they're mechanized but not automated so you have to give them hints on how to do the how to do the proof now when you get to code like the one I was showing you for the crypto code that's why we're using F-star and the fiat crypto group in MIT uses Cok and there are some people who use some other tools and there it's a choice between how much automation you want to get so if you in our case we use F-star because we can get some automation out of the SMT solver which F-star uses in Cok you do it via tactics and so on but you get more a small or trusted computing base so that depends on what your choices are but people have been using all kinds of tools for these harder problems so you mentioned the keyword I wanted to ask you is how big the trusted computing base is and does it have to descend all the way into hardware that's right so the crypto library I showed you Huckle-star is in C okay C is already like a big distance from assembly so we say okay if you really care about that you should use comm-cert and then you can get down to assembly okay you can get down to assembly but it still doesn't account for any of the micro-architectural attacks like Spectre and Meltdown that came up last year in fact none of the libraries crypto libraries out there is secure against them right now because they completely break our abstraction over the hardware itself so there is more work going on now after Meltdown and Spectre of people trying to link like the RISC-5 architecture or more novel designs like Sherry and other things from the University of Cambridge then take a formal model of what the hardware is supposed to do and then link it up and that's very fresh and cool area to work on but we don't have the answers yet so my question is about ProVerif so it must use some kind of decision procedure to actually go through all the combinations and find out that the attacker cannot obtain the message let's say and I remember somebody was talking about a similar tool and my question there was and so that's the question for ProVerif as well which is do you translate this down to something like a CNF that I can use a standard tool for it or did you hand code your own decision procedure and the reason that I'm asking this question is because if you do actually do like translate it to SAT then what you can do is you say well obviously you're looking for on set so usually that's how you work and then if it's an on set then a SAT server will actually give you a proof trace which tells you actually which parts of the protocol are completely useless obviously the proof trace doesn't actually contain parts of a proof I mean parts of the protocol that means that part of the protocol was completely useless to prove that the attacker cannot so basically you can essentially remove messages from the protocol therefore shortening it without losing any guarantees that you want to provide right now that's a very interesting idea so there are two or three tools that do compile down from protocol descriptions like the one I showed you to SMT and then they do try to use pruning they also try to use like Z3 will give you a counter example which you can then reconstruct into an attack for example so there are lots of interesting things you can do once you're using these off-the-shelf tools Proverif on the other hand is sort of highly focused on crypto protocols so what it does is that it has its underlying it is a standard horn clause resolution algorithm with selection where the selection is actually programmable it's nothing you wouldn't have seen 20 years ago in some sense but the heuristics that are going into it are all about how to use the selection procedures to kind of grade it in a certain way and as part of those selection procedures and heuristics it is trying to prune by figuring out dependencies but it does this in a way where it uses the structure of the protocol and what it knows about how these protocols usually go to really encode a lot of heuristics and other tools that have tried to do this in a more generic way by just compiling to SMT2 or something and losing a lot of structure in the process have struggled to kind of handle the complexity because the resulting formulas tend to be too big and this has been a limiting factor so as we've used both SMT and Proverif so I'm seeing such big advancements now in the last few years in SMT that it might be the case that soon we may not need all of these special heuristics and we might be able to use something more generic but it's not yet clear I would say in that field the custom decision procedures are doing better still significantly better for the questions it's not the case so then let's link again Patrick


My name is Mikaela Logan. First Lieutenant, I'm in 2-6 Cav Alpha Troop. Today, because we're conducting training, right now the Apache's out so that they can get some gunnery and range time just to stay on top of what our mission is. As attack helicopters, a few of our missions are to attack recon and security. So a lot of what we do is working with the troops and keeping them safe on the ground so that they can conduct their missions and everyone just stays safe. To prepare for the mission, we do ranges, semi or annually, and we'll come out here to the big islands away from Oahu and we'll just, we'll come down range, we'll shoot rockets, we'll pretend shoot missiles. I believe the goal is to make confident leaders and confident aviators so that when we go out and we're, you know, fighting wars and we're against the enemy, that we'll be able to confidently make decisions and we'll be able to attack, recon, pull security so that we can keep everyone safe on the ground in the air and that we can come home safe to our families. It's super fun. We're having a lot of fun out here. It's a hot sunny day. It's really beautiful and I think everyone's having a good time and learning a lot.


Hey, good morning everyone. Welcome to the session. Let's begin this time with a word of prayer before we start off. Anyone of us can pray please? Let's go ahead. Anyone can pray. Successful. Do you like to pray? Okay, let's pray. Father, we thank you for this time. Thank you for giving us this opportunity to come together. But we pray that even as we study a word and learn the God, I pray Holy Spirit that you will minister to us. But we pray Holy Spirit that our hearts will be open to receive your word, to apply your word in each of our lives. We thank you Father. In Jesus' name we pray. Okay. We last week we completed chapter 20. We looked at retirement, saving, retiring and beyond. Saving, investing, retiring and beyond. Today we go to the last is chapter 21 and chapter 22. Chapter 21 is entrepreneurship. Now we talked a little bit about entrepreneurship earlier on. But let's just look at a few scriptural insights on. When we talk about entrepreneurship, it basically means whether it is starting your own business, small-scale or big-scale business, or if we translate it to what we are doing in the for the launch. Luke 14, 28 and 30, if one of you is planning to build a tower, you sit down first and figure out what it will cost to see if you have enough money to finish the job. If you don't, you will not be able to finish the tower after laying the foundation and all who see what happened will make fun of you. You began to build but can't finish the job, they will say. Now entrepreneurship is a gift. And many of them say it's a gift that people are born with. So some of just had that entrepreneurial skill, the skills to develop new products, develop new ideas. But in entrepreneurship, we must understand that even before we start something, we need to plan it well. Right? So the worst here, the Lord Jesus is talking about in Luke 14, he's talking about this. He's saying, if you're planning to build a tower, first sit down, think about how you're going to do it. Plan it out and then start, lest you start. And then you're unable to finish it and people are going to ridicule you. Right? So be clear about the ideas, the business model, the business plan. Not at all on paper.  Now if it's a ministry that you're starting, you're planning to start, it can be, it may not be a church, but it could be something small that you're planning to start even in your home. Prepare well. Put down pros and cons. These are the pros. These are the cons and see how you can navigate between the cons. Because when you have a long list of challenges or cons that you see, you need to develop strategies on how you will face those challenges even before you launch something. Right? Be diligent about these things. The idea, the business model, of course the other things will be your values, your way of raising up leaders, financials, everything. You've got to be clear on how you do that. Right? Now secondly, determine to do business God's way. Apply biblical principles to develop your business. Right? Now especially if you're in a corporate setting, doing business God's way is important yet challenging. Right? But we can apply biblical principles to develop our business. Now when we look at the world, a lot of organizations use biblical principles. They may not believe in the gospel or they may not believe in the Bible, but biblical principles are definitely being used. Right? Joshua 1A says, and don't for a minute let this book of Revelation be out of mind. Ponder and meditate on it day and night. Make sure you practice everything written in it. Then you'll get where you're going. Then you will succeed. Now you take the context, followers, sorry, this letter written to Joshua. Joshua is writing it and he's talking about, he's reminding the people. Right? He's reminding the people of Israel who have come out of this 40 years gone into the Promised Land and he's saying, don't let the book of Revelation, meaning don't let what God has spoken to you. You know, just be thrown out of the window, ponder on it, meditate on it and when you do that, you will succeed. Now in terms of making decisions, right? Because we all make decisions preferably. So certain questions that we can ask ourselves, right? When we're making a decision, do you want to make the decision alone or if you have partners, do you want to make the decision with partners? Who would be your, you know, your co-founders?  Do you want to retain control or the power of attorney for the entire organization or do you want to split it up? How are the, how is the capital, meaning the resources being brought in, how are the resources being sent out? All these decisions must be done God's way, right? So when we look at God's work, I'm sure there are, there is a lot that we can learn, right? Entrepreneurial mindset, motivators, behaviors, character development, you know, timeless principles that we can use to establish kingdom priorities, kingdom focus and especially if it's a church then you've got to be full in if it's your own ministry that you're starting. Even though it's small, you know, we need to have these in place and biblical principles. You know, when a church is small, you may be getting about example, right? Maybe 10,000 rupees as your monthly, you know, tithes and offerings, right? I'm talking about a very small church, right? But as the church grows, you have 100, 200, 300 people, all of a sudden there's a lot of income, a lot of people are giving to the Lord then apart from tithes and offerings, people give for other, of other things, right? Within the church, people give as they are led. How will we, you know, use those resources? How will we use the money? Are we following biblical principles, right? So these are things when we start small and we have these things set in place as we grow and follow the same pattern, right? Three, don't be distracted by quick success. You are in for the long haul, Proverbs 2021. The more easily you get your wealth, the less good it will do you, right? If we experience quick success, it's wonderful, it's great, but don't let it distract us. Stay focused on the vision, the mission, stick to the values and the cultures that you have set in place. When we look at, you know, if you look at the corporate sector right now in our nation, there are, there are a couple of organizations that we know of, especially, you know, now with online things going online, these, you know, apps that are coming in, you know, success is very often it can be, if a product clicks, it clicks and success can just happen overnight, right? When I say overnight meaning in a short time itself.  Now, all of a sudden, so for example, you have 50 people, now they're maybe 500, 600 people, you know, period of six months, it's very easy to get distracted with that success. So it's good, it's good to have success, but it's also important that you stay the course. God, this is what the organization stands for, whether we are 50, whether we are 500, this is, these are certain things. This is the vision, this is always there in front of us, and we will stick with these values, right? So don't be distracted with quick success. I would say that when success comes in stages, it's more tastier. It's beautiful when success comes in stages.  Success just comes, it falls into your lap. Don't be distracted. Don't be hasty for profit. Proverbs 28-22, a man with an evil eye hastens after riches does not consider that poverty will come upon him, right? Now, profit is important, whether it is, you know, in any organization, nobody's running a charity, right? If you're an entrepreneur, you started your business, you're running it for profit, right? You obviously want to see your profit. If it's ministry, you're not running it for a profit, you trust God to just meet our needs, and to provide our needs, and to continue to be a blessing, especially if you're in the corporate sector, don't be hasty for profits, right? There will be times when you can take shortcuts to make a quick profit, but refuse it, right? Don't compromise on your principles, on your values just to see success, right? Build strong even if it means it takes time, right? Even if it takes time, you build yourself strong. Don't take shortcuts, right?  They have the desire, they want to do it, and they want to do it. They generally want to grow on the law, they want to do it. And one of the questions I ask them, and I purposely ask, is not to bring condemnation, but the reason I ask is so that they can help think and improve themselves. And I say, so if you want to get to this place of preaching, teaching, ministering to people, and doing all of this, go by stages. They eventually, what happens is they want to, from one level, they immediately want to go to the highest level, and that's normally how God does not work. God does not work that way, right? He doesn't, normally he doesn't do it. He takes us through stages. But one of the things I always ask them is, how much time are you spending with the Lord? And many times they say, you know, maybe half an hour, 45 minutes, and I tell them that's not enough. Now if you desire something that is really high, of course there's God's grace, that you know, God does not, you know, we're not going, we're not asking, you know, God, I'm going to pray for three hours, will you make me, give me opportunities, and that's not the point. The point is, when we want something, we got to do, you know, there are things that we don't know, God to minister to us, use us in our nation and the nations and all of it. There's a work that we have to do, right? We have to go back, spend time. There is a sacrifice. There's a price that we must pay, right? And of course, when we do that, when God opens those doors for us, it is wonderful because we're not hasty for profit, we're not hasty for success. And when we go through those stages, it's beautiful. It's basically building a foundation for us, right? First, plant your fields, then build your barns. Proverbs 24-27 says that first, plant your fields, then build your barn. If you build a barn without planting your field, it's going to be empty for a long time until the harvest comes. And if you have built your barn, but you have no plantations in your fields, that things, it's of no use, right? Stay focused on what is important and work hard. Let me just picture this. You have a field, right? And there's a barn, but we haven't done any plantation, right? What is the use? We should first plant, and as the plants are growing and you know it's time for a harvest, you build a barn so that whatever is harvested, you take it, you put it in the barn and everything is settled in the right way. The barn can be built once the fields have been planted, right? So plan or see, remember we talked about this, know what is important. No, when we talked about, I think it was work-life balance, know what is important. That the barn is important? Yes. But what's more important than the barn, the plants, right? If I don't do the A and I'm directly going to the B, who will do the A? Right? So first plant your fields, then build your barns. So basically what we're trying to say is do what is important first and out of that do the other things, right? One of the important things that I always tell when I meet, you know, very occasionally we meet pastors from different villages and rural areas. The first thing I ask them is, have you registered your church? And most of them don't even know what is the vision. They don't, there's no vision. This is a church, you know, we don't blame them because they just started off their home and not very learned. Things I encourage them to do is get to a lawyer and get the church registered. Because when you do that, you're doing it in the right way, right? Keep a close eye on what brings in the bread and butter. Proverbs 27, 23 to 27. Look after your sheep and cattle as carefully as you can because wealth is not permanent. Not even nations last forever. You cut the hay and then cut the grass on the hill sides while the next crop of hay is growing. You can make clothes from the wool of your sheep and buy land with the money you get from selling some of your goats. The rest of the goats will provide milk for you and your family and for your servant women as well. So as your business takes shape, there will be many things that are critical, many non-essentials, many non-critical things that come up. There are many things that can come as distractions. Now choose, there are opportunities which may come in which we may have to say no to. Stick to what is good for your business. Now when we look at it in a, when we talk about ministry, there will be many opportunities that come our way. Now we must carefully see, is it in line with what I want to do? Is it in line with the ministry? Is it in line with the vision? Is it going to be something that is going to build the kingdom of God at the overall picture? Is it going to bless people's lives? Is it going to raise up discipleship? Or is it going to increase in ministry, evangelism? Are these things going to happen? So choose, think about what is, keep a closed eye whether this is the entrepreneurial sense, your bread and butter, meaning when your income, where is the place where you get the most income. And in the ministry side, where is the place where you can be more effective? And so think about that as well. Keep a close eye on the core of your business or the core of your ministry. Stay clear of pride that comes with success. Probably 16, 18 right goes before destruction and a haughty spirit before the fall.  But as the business grows, as the ministry grows, stay clear. This is a hard condition. Stay clear and stay away from pride. Always acknowledge God as you continue to walk in humility, continue to operate in the principles of God. And we all know this structure is dangerous. Whether it is in the corporate, whether in ministry, and it's sad to say that right now when we look at ministry, you know, pride has caused so much, so much of trouble. And many leaders have fallen because of pride. So that's a hard attitude. We need to make sure that we don't fall for it. Your personal income and benefits keep it right. Now, for example, you're an entrepreneur, your business is growing.  So, you know, pay yourself well, there are benefits within the organization, organization, use it, but let it be equal to all of them who are in the workplace.  And when you also, when you do this, also make sure that you're not indulging yourself too much, right? Avoid excesses, avoid things that you feel that you wouldn't need. You know, you don't have to live to prove other people. You see what you need, what is needed for you, and that's more than enough, right? We don't have to live to prove, hey, you know, see, this is what I do. This is what I don't have to do that. So basically, this is walking in humility and keeping things right. Multiply what you have by empowering others. Matthew 13, 31, and 32, Jesus told them another parable, the kingdom of heaven is like this, man takes a mustard seed and sows it in his field. It is the smallest of all seeds, but when it grows up, it is the biggest of all plants. It becomes a tree so that the birds come and make their mess on its branches. Multiply what you have by empowering others. You can empower other people in many other ways, like providing education, paying for their education, providing them with small job opportunities, you know, providing them with, you know, family benefits, health insurances, simple things, right? Medical health. You can empower others to be self-sufficient, right? By helping them start small businesses, you know, rural, in rural settings. And what about in ministry? You know, this is what we are called to do, right? Empower others, raise up other leaders. So we do that. We help rural churches, smaller churches, smaller ministries, plant ministries, build ministries, and we're able to look after them. So multiplying by empowering others. And then finally, the woman entrepreneur can be a virtuous wife, mother, and homemaker, right? Now, as a woman, right, speaking to all the women here, God has called you to be an entrepreneur. Wonderful, right? But also be a virtuous wife, mother, and be there for your family, right? And it's wonderful, right? And we always believe that men and women are equal. God has created us alike. We have the same Holy Spirit inside of us. So God can use us powerfully, woman. God can use you powerfully, right? Or give you wisdom to start businesses, multiply businesses, you know, to be a manager of both the house, the family, the children, and also be an entrepreneur. And this is wonderful. Because when we do this, you know, it's a virtuous woman as the book of Proverbs talks about, right? So we complete this chapter, let's get into the last chapter, chapter 22. Any questions? Any questions on this chapter? I know we just, we're just touching the entrepreneurship is a big, big topic. We can talk about it for days. There's a lot of material, but these are just a few pointers. And I'm just trying to translate both in the workplace and in history. So any questions? Shall we get to the last chapter? It's a small chapter, workplace transformation. Okay, so workplace transformation, what is transformation?  We can change things around in that sphere of influence, right? Now, how do we do that? It's not going to happen overnight. It's not going to happen just by, you know, just by doing it on our own strength. Workplace transformation happens when we, when we use the principles of God, when we have certain godly principles, and we begin to reflect that in our work, right? And each one of us, you know, wherever we are, it could be the most meager job that we're doing. We can cause a transformation. Now, it could be just, you know, three or four people believing in, you know, or seeing us and three or four of our colleagues seeing and talking about us. That's a workplace transformation because things are changing. People are looking, people are watching. So let's look at a few points on how you and I can be agents of transformation in our workplace, right? First one, initiate a culture shift. Matthew 5, you are the salt of the earth, Matthew 5, 13 through 16. You are the salt of the earth. If the salt loses its flavor, how shall it be seasoned? It is then good for nothing, but to be thrown out and trampled under foot by men. You are the light of the world, a city that is set on a hill cannot be hidden, nor do they light a lamp and put it under the basket, but on a lamp stand, and it gives light to all who are in the house. Let your light so shine before men that they may see your good works and glorify your father in heaven. What a wonderful example Jesus comes up with, right?  Salt permeates, light penetrates, right? And as followers of Jesus, salt and light, both influence our environment, both influence. Imagine there's darkness and you switch on the light, there's light. The light is not thinking twice, oh, should I come on? No. And if there's food without salt, it could be the most expensive food, but without salt, it's going to be tasteless. The moment you add salt to it, it is transformed. The taste changes. When you're in a dark room, the moment you switch on the light, the place is transformed. It's gone from darkness to light. And we have been commissioned.  And wherever you are, we can influence the world, right? We can influence the world by initiating a culture shift, a change in the mindset that accepts things the way they are, right? You do this by walking in the timeless principles that God has for us. You do this by walking in the character of Christ. Wherever we are, we can be salt and light, get commissioned to be that. Now, is it going to be easy? No. Is it possible? Yes. It is definitely possible, right? And I have plenty of examples of, you know, remember this happened in, I forget which revival was this workman's revival. I think it was that where these two men who were in the corporate sector happened in the early 1800s, early 1900s, who were working businessmen. And one of them had this whole, you know, reading the Beatitudes, had this whole thing, hey, I've called to be salt and light, but I'm not doing anything about it. So he decided we will begin a prayer for 15 minutes in the office during the break time. And this is when during the time there was no cell phones, no, you know, laptops, nothing, right? And they started this prayer. And this prayer went on for many, many, many years causing a whole outpouring, a whole revival started off with two people. And we talked about revivals of God, I mean, saw the Welsh revival, the different revivals that happened over the years, all started off small, but it shifted the culture of the entire society, right? We can be an initiator, so culture drift in our workplace, wherever we are. Create a constructive change, Matthew 13, 33, another parable he spoke to them. The kingdom of God is like leaving, which a woman took and hid in three measures of meal till it was leaving, right? It only takes a small amount of yeast to affect the entire dough, which is mixed. The kingdom of God is so just a little bit of yeast is able to affect the entire dough. Just a little bit of the glory of God, the power of God, and God using just a few of us can affect the entire dough. The entire workplace can be changed. So what do we need? We need the power of God. We need the power of the kingdom, kingdom values, kingdom authority to be released through us. We start small.  Now there's no need. And that's not true. There is a need for revival. There is a need. There is so much need for a revival. And when we look at, you know, the book of revelations and we talk about those three and a half years, great tribulation, look at a great world revival that is going to happen through the two witnesses and many other believers. So revival is needed. It's a constant. It is needed every moment until the coming of the Lord, right? So create constructive changes in the workplace, right? In an environment where there is dishonesty and corruption, step in and demonstrate integrity and challenge people to do the same. In an environment where there is hostility and strife, step in and demonstrate love and kindness. In an environment where there's injustice and abuse, step in and demonstrate justice and the goodness of God. In an environment where there is greed and self-aggrandizement, step in, grandizement means self, you know, there's this pride or a feeling of, you know, wanting to be known and famous and popular. Step into the place and challenge and demonstrate sharing and generosity. Now, trying to be a change, you know, trying to be this salt and light calls for wisdom, calls for courage, calls for strength. People may ridicule, people may mock at us, but you know, if God has called us to be salt and light, we are to do our best for it to be that right. Next one, be a transformational leader, John 10, 11 through 14. I am the good shepherd. The good shepherd puts the sheep before himself, sacrifices himself if necessary. A hired man is not a real shepherd. The sheep mean nothing to him. He sees a wolf come and runs for it, leaving the sheep to be ravaged and scattered by the wolf. He's only in it for the money. The sheep don't matter to him. I am the good shepherd. I know my own sheep. My own sheep know me. There are two kinds of shepherds. Jesus is talking about here. One is a shepherd who is a good shepherd. He's looking after his own sheep. Even if a wolf comes, he's willing to stand for a bear or a lion. He's willing to stand, put his life on the line to protect his sheep. We have another shepherd who is if the sheep is not his and the moment he sees his life is in danger, he's going to run away and the sheep are destroyed. Which kind of leader do we want to be? Good leaders care and serve the people they serve the people they need. The others do it just for themselves. Now, you and I are called to be transformational leaders. If we want to transform an organization, if we want to transform communities, we need transformational leadership and we can use this value. This value that God is teaching us. Be there to care, to protect and to provide for your team. Teach them. A good shepherd does not only love and care, but he also corrects and instructs. Leads them in the right way. We got to balance both of these. There's love, there's care, all of it, but there's also correction, instruction, exhortation. All of it should be there in a transformational leader. Finally, last one. Demonstrate the kingdom in the workplace. Acts 17, 16 and 17. Now, while Paul waited for them at Athens, his spirit was provoked within him. When he saw the city was given over to idols. Therefore, he reasoned in the synagogue with the Jews and with the Gentile worshipers and in the marketplace daily with those who happened to be there. So later on, we see in this chapter, Acts 17, we see that Paul goes on to preach in Athens and what happens? There's a shift. They call him to Mars Hill, the place where the aeropagus, he preaches the gospel there and people believe in Jesus and a church is started. What happened? He demonstrated kingdom values. He demonstrated the power of God's kingdom in that place. God is interested and God is involved in our workplace today. Our knowledge, our science, technology and all our intellectual prowess we have gained have divested the workplace from the presence and the power of God. But remember, it is God who gives us the knowledge, the wisdom, the technology. Everything was given by God. So we need to let people know how to experience and how to walk in this knowledge of God. There are a lot of things that we can do. We can always rely on the supernatural. There are things that science and technology cannot explain. If you've got a friend in the workplace who can share this many years back, this man is a friend of mine in the workplace. Not a friend, but he would always walk and ridicule and he would be really upset whenever he sees me. He would be angry. But one day he came up to me and he said, you are this Jesus boy and all right? So this is what's happening at home. Mother is going through this sickness, this illness for many years. I'm not going to ask you to pray, but if there is a God, my mother is a good woman. She lost her father in the young age. She's the only one that is there for me. Even if she dies, anyway, I don't believe in God. So what kind of a God will do these kind of things? And he was just upset and angry with me. And I remember telling him, hey, it's the way God works with people. It's not God's fault. He was not willing to listen. And I remember telling him, can we pray for your mother? And he said, you pray. I'm not going to pray. And we pray. And I remember after a couple of days, he came back and he said, my mother's discharged from the hospital. The doctors don't know how everything became all right. And this really changed his mind. He stopped ridiculing, mocking. He stopped using overtime. He stopped using bad words. He stopped getting angry with people. And next thing I noticed that he would come and sit next to me every time when we were in office. And he began to spend a lot of time with me. He began to come for those morning prayers which had started. And God just changed him. Just there's a big transformation in his life from this arrogant, rude person to just being quiet and very humble. And I'm surprised of his humility. He became so humble that it didn't matter to him what people say, what people spoke. He was very humble. How is that because of the Holy Spirit? And God is calling us to demonstrate this kind of kingdom principles in the workplace. Wherever we are in our workplace, in our communities, pray that God can use us through the gifts of the Spirit, through the anointing of the Holy Spirit to demonstrate values of God, wherever we are. So that way we will truly be salt and light. All right. So we have completed our portions. Thank you so much each one of you for joining along. I really enjoyed studying this and reading and teaching this entire book. And I just pray and believe that each one of us, including me, we will continue to use these principles and continue to reflect on them, use them for the glory of God. Any questions? Any thoughts before we close for this semester? No questions? All right. So let's just close and pray. Maybe one of us can just pray. Just thank the Lord for this entire semester, for this entire study and close. Anyone like to close and pray? Yeah, let's pray. Dear Heavenly Father, we come to the end of the name of Jesus. We thank you for this day. We thank you for this course. Whatever we have learned, Jesus, we thank you for guiding us throughout this whole course, helping us to understand a lot about how to conduct ourselves, how to reflect you in the workplace, Jesus. God, I pray that whatever we have learned, we will put it into practice. We will be doers of the world. Let us not forget anything that we have learned so that we can glorify you through our life, through our actions. No matter where we go, we can reflect you, your love, your kindness, your compassion. And God, we can lift your name above all else. I thank you for all my classmates. We thank you for Pastor Paul. We thank you for blessing him with your knowledge so that he can be a blessing to others. Be with us and guide us throughout the session. We thank you for this whole semester, everything that we have learned. We give you all the glory, all the honor with a grateful heart. We say a big thank you to you, Jesus. We love you and we honor you. In Jesus name I pray. Amen. Amen. Thank you, Jafina. Thank you, everyone. Have a wonderful break and I'll see you next semester. God bless. Bye now.