Thank you. Hello. Okay. Yeah, so thanks Pedro and thanks very much for the invitation. So yes, in this talk, I intend to present some ongoing research on TLS and HTTPS and the number of project is double address. So I first have a few slides describing broadly what you are trying to do then you have a demo. They will go into more details about cryptographic algorithms and crypto protocols. So needless to say HTTPS and TLS are critical. So the the actuality there is that in fact more and more people are consolidating around fewer protocols. So doing your own protocol is considered an idea. So everyone ends up using standardized protocols and TLS being the easier to use. It's maybe running something like trillions of connections every few days. In fact, most of the Internet traffic is now encrypted using TLS and it will become a mandatory with HTTPS2 and moreover, there are lots of other things like VPNs, voice, emails protected by TLS. So it's quite a complex system at the same time from especially from a verification view point. It has the big advantage of being relatively small. So there is some cryptography, some protocol, some PKI and in the protocols there are crypto protocols and application-level protocols, but nonetheless, we can hope to implement it all in tens of thousands of lines of high-level programming languages, which makes it, we hope, a reasonable target for full verification, which will not be the case for a SEO browser or a full-fledged operating system. It's also quite as is well-known quite broken and in fact it has been, we have seen a succession of attacks, discoveries, improvements and fixes over the last 20 years and the issues range from most practical but boring ones like buffer overruns or failure of memory safety to implementation design issues such as problems in state machines, so logical flaws in implementation to misunderstanding about how the different bits fit together and it must not be the case for the PKI. There are also some specific issues due to cryptography with weak primitives or primitives that used to be okay and now are broken and plenty of such channels. So more fundamentally, one of the big issues of the ecosystem is that the security is quite often implicit. So there is not a clear well-agreed precise notion of security for TLS or HTTPS. And maybe as a result of that, APIs tend to be low-level and quite dangerous and even in some cases we discovered some flaws in the standard, so for the triple uncheck attack for example, if you implemented the standard you are subject to the attack. So the practical situation is that we have mainstream limitations that get patched regularly. So if you look in last year for OpenSSL, there were 33 CVs resulting in two patches. So it's a few amounts. So it's reasonably safe to say that OpenSSL has never been safe so far. There was always some open attacks in there and well, we should be able to do better. So what we propose to do is to rebuild a stack, HTTPS stack, one component at a time, with strong machine checks of safety and security for every component. So at the same time we are, and that's maybe half of the project, which I'm not going to talk much about it today, but we are developing verification tools, programming language and compilers who support that effort and by co-developing the tool, we are hoping to improve both to the point where we can verify something at this scale. Finally, and in contrast, maybe to some of the work building reference implementation, we would like our components to be usable. So we are aiming for things that are verified, formally verified, but also reasonably engineering, not to demanding in terms of resources and reasonably fast so that they constitute a reasonable alternative, not just something formally verified. So we have a composite team involving essentially four labs, so three labs at Microsoft Research and one in Paris at Inria, with a mix of systems, security, cryptography and programming and verification. So one question you may ask is why are we still looking at that problem? In a sense, TLS is just a secure channel so that has been well-studied and solved maybe a decade ago, maybe a bit more and so something to keep in mind in the talk and that I tried to illustrate as we go and is that there is a cryptographic viewpoint to the protocol, but they are also quite different and conflicting viewpoints and the lack of communication and synchronization between those viewpoints has led to many persistent difficulties. So let's start with a cryptographic viewpoint first. So we have and that's essential for the design, but we get papers, typically, that look at one aspect of the protocol at a time and to get something readable, simple and tractable, they tend to ignore all the other details, have another relevant for that particular property. And so we get something that is nice and simple and intelligible, where you can actually convince yourself by wrong that the proofs are correct. But they do not compose and if you try to put all the components together and get all the security properties, there will be lots of details that are going to get stuck in there and in our experience in particular, we expected we were able to reuse existing cryptographic results, paper results in the work and in many cases we could reuse the ideas and the methods and the proof techniques, but not quite the results because we need slightly stronger assumptions or an extra oracle or some cryptographic agility or some joint assumptions in places. So in any cases, what is pointed to as the reference for the design is not quite good enough to check even the cryptographic protocol as standardized and used. At the other end you have the RFCs and RFCs are specifications that they are, it's English, so it's very informal and moreover they focus on the wire format. So the main point is interoperability, not quite security and things are getting better, but still security is considered, it's not specified. So you have a section that says security considerations and they discuss things to be careful about or to think about when you implement it or when you use it, but it's very far from a precise definition of what you should verify as a security property. Then we have the viewpoint of the implementer, where the main issue is typically not cryptographic security, but more mundane issues like memory safety and integration and how to handle graceful errors and also how to have a system that can be that is operationally secure, that involves a lot of care about being able to upgrade and to maintain the system and to evolve it over time. And finally, we have the user of the protocol who tries to use those standards and implementations, but because security is loosely specified and because the APIs are quite low level, in many cases they end up misusing or misconfiguring the system. So they were a very nice paper by Vitaly Shmetikov and his colleagues a couple of years ago showing that 80% of people using TIS libraries were getting the configuration wrong, so that any certificate would be considered as valid no matter what the subject was in that certificate. So it's very superficial, but it validates 80% of the deployment. It's much more serious than cryptographic vulnerability will be. So as you may know, we have been working on TLS for a bit longer. So we started with me TLS in 2013. And there the goal was a bit different. So we really wanted to understand why the protocol was secure and to build a reference implementation, not something directly usable. So we tested the reliability, but certainly that performance. And it was only up to TLS 1.3 and there were quite a few limitations. So we were excluding the actual cryptographic primitives and construction. So we were really sticking to the letter of the RFC. Also, the proof was machine supported, but not fully mechanized. So we had for the main cryptographic argument for the handshake and for the record layer, we had paper proofs. And in some cases, the synchronization between the two was quite delicate. And finally, it was good enough to test it in particular use it to look for attacks systematically. And that was one of the way we found most of the state machine attacks. But it was not good enough to be deployed. And in a sense, developing a verification and using only to find bugs elsewhere is a bit disappointing. So this time we want to get the tools right so that we can actually deploy what we are trying to build and verify. So the way it works is we are consolidating a report on a new programming tool chain based on the programming language that is oriented for verification. And that is an F star. So it's a language I'm going to review a flavor of that language later on. And we use that language as the one language for coding everything. So we have the implementation code, including the level code. You also have the specifications. We have security definitions. We have cryptographic games. We have cryptographic constructions. And you also have the proofs. And so everything is packaged together, can be verified together. And then from that, we can conduct verification. And once we are satisfied that everything that is specified has been checked, we can erase the proofs and the specification and just extract lower level code. So we get to CC++, but we will not be able to conduct the proof and the modular reasoning directly at the level of C++ and sort of. So nonetheless, we realize that CC++ is unavoidable if you want to integrate with the ecosystem. So we actually spent a lot of time generating high quality readable code because we expect people to be able to conduct independent reviews at that level even if they don't understand the formalism we have. And at a lower level, we interrupt with the rest of the system. And so we have some testing. We have been running interobality for a few years on TLS-1.3, for example. But in summary and before we switch to the demo, what we build is a single model plus implementation with formal support. And we get two things out of it. One of them is that we can validate the design because we take an informal design and we formalize it as something very detailed, which is an executable spec in a sense. And at the same time, we get a concrete implementation where we can work in performance and get the security properties that we get on the design done to the implementation of the protocol. Okay, so I have a brief demo. I hope it works. I'm demoing two components of the system. So METLS, which is our implementation of the TLS protocol plus all the cryptography, the cryptographic primitive that are used to run TLS as a cryptographic provider. And so for this demo, I'm showing an integration in Internet Explorer. So we redirected calls from Internet Explorer so that METLS will be used instead of the default cryptographic provider so that we can experiment with TLS 1.3 and zero RTT using GE as a user interface. And as a server, we picked NGNICs, which is one of the fastest web servers. And similarly, we replaced its cryptographic component that usually is open SSL with the one component with verify TLS and verify crypto. And we also added support for tickets so that we can experiment early with tickets and resumptions for TLS 1.3. So here is the demo. So it's not okay. I'm not going to detail that too much, but it's Internet Explorer running with the debugger attached so that we can monitor the code to METLS underneath. And I'm using that because otherwise it will just work as usually just display pages. So if you load this page with lots of pictures, it's going to open many connections and do the multiplexing on top of that. And except for the debug information, you wouldn't be able to tell we are using or implementation or another. It's just fast enough at this level. So you can see at the top that, okay, if you look at the window below, if you are looking, we can see that we actually try to negotiate TLS 1.3. But in that case, we fail to negotiate 1.3 with our server, which is also implementing TLS 1.3. So that's our test server that has been around for experimenting with TLS 1.3 running NGX in the background. And so here we end up with 1.2. And the reason we do is because my client is using the 20th draft of the standard and the server is using the 21st draft of the standard. So I realized that this morning. So to show the actual zero RTT, I'm going to use the command line demo. So here I'm running OpenSSL as a client. And I open a TLS 1.3 connection to my NGX server running Meet TLS. And the first session establishes a ticket. And now I can, if I can find the right command line, yes. So I can then use the ticket that is established to open a fast connection. And there we can see that early data was accepted. So the very first request that was sending the first message on the network was processed as part of zero RTT. Because both ends could reuse the information in the ticket to establish keys without any additional entries. Okay, so that was the demo. That's quite minimalistic. So the next, what I want to show is what we do for verifying implementation of cryptographic algorithms. So that's what your level programming and functional properties of algorithm. And as a starting point, I wanted to show some typical code that you can find in OpenSSL. So that's a code for implementing. I think it's a too. And it's a mix of assembly and parallel, which is not quite what you would use for verification. And the reason is, of course, that people want to get the maximum speed out of it. So in OpenSSL, there is code specializations and different assembly for something like 50 different platforms. And it means you're using these kind of scripts, and it also means introducing bugs from time to time. So I'm going to show you what we do instead for one simple algorithm. So that's Poly 13.05, which is one of the fast, modern, one-time Macs that is used in TLS for authentication. So it's a multiplicative Mac. So it works by encoding your data into a polynomial, into the coefficient of a polynomial. Then you evaluate it at a random point and you mask the result. And it's quite secure. So, and those mathematical specifications are very simple. It fits in a couple of lines, as you will see. The implementation is more complex because it plays lots of tricks to go fast. So it represents numbers using multiple limbs, and it tries to save on the number of reductions and carry propagations that you do using different tricks. So it means that at the same time we can get a specification in F-star. So that's the first bit of F-star that I'm going to show today that fits in this screen. So it's literally a couple of lines. While we can also have an implementation that is optimized on that text together with the proof of a few thousand lines of code. And provided you understand and you agree with the specification, you don't have to look at the code. The verification is going to check that this is what is implemented by this optimized code for the platform or it's going to return to you an error at compile time. So let's look at the spec. So that's F-star syntax. So we define our prime. We define an element as a natural number that is smaller than the prime. Then we define addition and multiplications in that field. Then we have a noncoding of word. And then we have a recursive function that just evaluates the polynomial recursively. And that's what we are going to use and mask in the protocol. So why bother? Well, Poly 13.05 is relatively new. So new implementations are being added to existing implementations. And just in last year, there were three bugs, including one vulnerability report in OpenSSL, in the implementation of that particular feature. So one of them is a buffer overrun, which is boring but very dangerous. The others are just incorrect results due in particular to subtleties in the assembly code to do carry propagation. So instead, we are in F-star. But we want to have full control over the code that will generate. So in fact, we design a subset of F-star that is intuitively the intersection of F-star and C so that we get to a program at a low level and link with assembly code if need be, but still benefit from the full verification framework. And of course, we build a compiler so that once we have written and verified something in F-star, we can securely compile that done to C. From C, we use existing compilers, which is a big risk, but that's the one you are willing to take for now. There is actually a certified compiler named Concert built by Inria. And that's what we use for our formalism. So we prove that we compile to the semantics of C as used by Concert. And if you want, you can use Concert instead of GCC or MSVC to compile your stack. But if you do that, you are going to miss some optimization. So there is a performant cost in using a fully verified compiler. So concretely, here is, okay, it's not that readable, but I'm not going to read the lines, so don't worry too much. So that's one routine computing the last polynomial added to the Poly 13.05 computation. So that's F-star with the specification and the implementation. And it compiles to this, which is, if you could read the details, just C code, but with very clear correspondence in the operation. So in effect, we are mostly erasing all the specs and the proofs elements to get back to see. In fact, you can see that there is the code that is just copied verbatim, except for inlining some of the constants. And then we have memory safety specification that guarantees that all the pointers that are passed in and out are accessed as they should and that they are live when they are the reference. We have a math spec that relates to what I have shown earlier and that says what is the specification of what you are doing in terms of unbounded precision mathematical integers. And then we have a proof that applies to lemas to convince ourselves that what we do in the code matches the mathematical spec. So it is correct, but is it fast enough? Well, the good news is that after quite a lot of work optimizing both the compiler and the source code by my colleagues, we can match or even exceed the performance of the best in return implementation coded in C. So here you have the numbers given in cycles per byte. And as you can see, we are slightly better and even much better than OpenSSL for portable C implementations, notably for curve 2559. We are not as fast as assembly yet. So if you are willing to use platform-specific instructions, then we can't compete by writing code from F-star, compile to C. But for that, we have domain-specific language that does portable assembly and that gives you even better performance at your verification cost. So the tool is named Vale. It was presented last week at Eusnix. And the principle is the same. So here is the six instructions in the OpenSSL implementation. So here we just use exactly the same instructions in Vale, although they can be manipulated and assembled using procedures. And that was the instruction where carry propagation was initially missing, one of the three bugs I mentioned earlier. So this code is essentially unchanged and will be generated exactly as what you would use in OpenSSL or any target implementation. But you do have a mathematical spec plus memory safety specification telling you what the math is and also what registers are being affected by what you are doing. And there is also some explicit proof annotations to convince the prover that you are indeed complying with both the memory safety policy we claimed and the math specifications we gave at the beginning. So the design for that Vale language, so Vale stands for verify assembly language for for rest is quite interesting. So we embed the semantics of the platform in F-star so that it is platform specific but easily retargetable. And we treat the specifications and the description of the processor as part of the TCB but on the other hand the source code and the Vale tool that generates the code and the proof can be interested because the result of its work is going to be checked using F-star verification. So and performance is unsurprisingly very good so we match we can match any assembly that will compile on x64 probably we can prove it is correct. And here the number are slightly better but I will not read too much into it. I think it's a slight difference in the coding conventions that we use but by such chance we get the best performance for things like AES where using specific hardware acceleration is critical and where we will not be able to compete just writing SQL. Okay so that concludes the part on the cryptographic algorithm themselves. The next step is to look at cryptographic protocols and security rather than just correctness and safety. And for that a big part of our work has been focused on TLS 1.3 which is quite an exciting revision of the protocol so you I'm not going to say much about TLS 1.3 at all but it's the result of an intense and quite strenuous discussions involving cryptographers, engineers and many users of TLS. It's more modern it removed a lot of the bad cryptography that led to the use assumptions for TLS 1.2. It has fewer round trips and so it should yield significantly better performance as well as stronger security. So for us it's exciting because new implementations are required for all and so the fact that we are developing implementations from scratch is less of inconvenient and at the same time it's very important for us to complete as much of the verification as we can before the draft turns into a standard because it is still or it was still relatively easy to make changes or to improve the protocol and it's going to get incredibly hard so for triple and shake attack the time to patch the protocol with the mandatory extensions was three years which is just too long. So what the status is so as I said it was quite active and complicated process so we are at the 21st draft and we were at the final call but we went back from final call to do a bit more testing before going back to final call so in short it's almost ready to be turned into an RFC but not quite and it took much longer than expected. Also from our viewpoint several proposals that we made were implemented in the standard and we think they lead to stronger security they certainly need to stronger guarantees in all the models we have considered and so they include findings from our work until it's 1.2 and also more smaller scale designs against don't buy resilience and fine prints in the new standard so interestingly we also introduced a new attack in one of the drafts by fixing another but gladly we fixed it before maybe I think it for after one month it was fixed so this happens but we have to we will not trust ourselves with most of the changes otherwise. So where do we are in terms of implementation so Mitziel S is coding in FSAR today it has been running and cooperating with several other implementations for one year we implemented many variants of the standard so we are at TLS at the draft 1.3 it's still partly verified so we still have to complete an integrator work on verifying the handshake which is also coded in Okamal I'm not compiled to see yet so what I'm going to focus on today is work that we did complete for the record layer where we generate C code and we have completed verification for that part linking to the verified crypto that I presented earlier. Okay so I have a few slides showing what we mean by actual cryptographic verification in F-STAR and the goal of those slides is to convince you that what you are doing in F-STAR is not so far away from what cryptographers will do typically on with open on paper proofs using a game based code based reductions to convince our fellow security of their system so so we so we don't have functionalities instead we have actual implementation module so each box represents an F-STAR module which implements some functionality with some well-defined interface and so we use them for everything so for the implementation itself but also for modeling games and cryptographic assumptions and we use the very precise type interface of F-STAR including the mathematical specifications if need be and also modeling of stateful effects to capture what these primitives are doing and also what security properties we expect and so the the idea is that to capture in the formalism at the level of the interface all the properties you are going to rely on cryptographically in our proof so I have a very basic example to to clarify this method which is to look at message authentication codes which is hopefully the property that we want for the poly-1305 algorithm that I've shown earlier in the talk at least for a single message so if we look at the interface of a mac library it's not going to say much about security at all so it's going to have a function for generating fresh keys a function for making messages and the functions for verifying messages and it may specify the length of the tag or the length of the key but it's not enough to reason about security so instead we write an ideal interface that captures the the essence of security notions that you are that you are going to rely on or if you are constructing something trying to establish and so for mac in these specifications we are relying on a log so we have a log which is ghost it it doesn't exist at runtime but nonetheless we can use that log to specify what ought to happen with a perfect implementation of a mac so when we generate a new key we said that the log for that key is empty when you make a message we add to the log the message together with its tag and when we verify the message the result is exactly or has to conforms with the result of the lookup in the ghost log that you are maintaining and so if you think of it it's very close to a ufcms security in fact you can show that it coincides with data and it's great for verification because once we have this log and we can reason about it we can reason about the log at the other end of the communications and that's sufficient to do conduct or protocol level proof it's not so great from realism because we know that tags can be guessed so our type system would reject any implementation that may fail because the tag can be guessed and so so we have to do a bit more before we are able to use that nice specification to continue with the high level proof of the protocol so to do that we also use fstar to program a game and so we have a game that defines ufcms security you know so it's quite the classic definition except that it's for mic instead of signatures and so in the game we generate a key we also have a log so it's essentially the same log and you have an oracle for encrypting messages and the attacker gets the oracle and tries to produce a forgery and then we check whether it is indeed a forgery by verifying that it works and also checking that it's not in the log so that just a naive transcription of the game that defines ufcms and now from that game we can we can reduce deviations from the ideal interface that you like to use to verification to an attack against that game so that goes as follows so we have a concrete protocol it's an rpc we have a mic implementation that is assumed to be ufcms but only computationally so we introduce an ideal setting that you are going to jump to in a single game step and we have a filter that is going to use the log to correct all the forgeries and because we correct the forgeries we have the nice unrealistic spec so we can verify everything and conclude the proof of security for the full protocol by typing however we still have to go back to the real world and so we can also check by typing that anything that composes with the radial mic interface is actually a valid ufcma adversary and that the real system is secure except with the same security loss as the one incurred in the game that defines ufcma so that's a very simple example but that's the basis for most of the proof that we do in f-star so we don't do any deep cryptography but we can compose existing and you can formulate and compose existing game-based notions of security for all the primitives used using tls for example so for example i'm going to show get into more details about the record layer so there we need more than authentication we need authenticated encryption and we can write a game that defines authenticated encryption as you would expect and we can transcribe that into a game written in f-star and capture its security by typing again to go once we have defined that game move to a world where we can use step shaking and automated verification to propagate the guarantees given by this this game so the constructions we are going to do is for the record layer so it involves combining a mac and some encryption so here i'm not going to give you the details for it but i wanted to give you the details for something that you everyone who already know which is encrypted and mac and so in that case we have two modules with that require some cryptographic idealization so we first idealize the mac as i've shown before using the ufcma assumption once we have that we can verify by typing that we comply with the in-cpa interface because we are never going to decrypt a message that wasn't encrypted before so the encryption is by lookup not by actual decryption at which points we match the interface to idealize the encryption and then we wish we can idealize and by combining the two we can verify without any new security assumptions that the uncridden mac constructions give the guarantees associated with authenticated encryption and so that's the general structure of the proof so we have a module that captures any cryptographic assumptions you are making and then you have a systematic way of composing them using flags to control idealization so technically we are going to verify the code no matter what the flags are because we don't want to verify separately each of the intermediate games in the proof so the proof goes for all the games that are going to be spanned in the proof and then to conclude the proof at the top level we just need to switch the flags one at a time to conclude so which is completely generic within that setting so okay so let's go back to TLS so the regular for TLS is the same except that there are lots of standardized complications in particular there are many keys there are many algorithms there are many constructions there is also a fancier model for key compromise where both algorithms and keys or intermediate secrets can get compromised and then there are engineering details like fragmentation padding and state so it's probably worth doing because although it's less if maybe more mundane than verifying the handshake it's a place where there were historically lots of bugs in TLS moreover it was at the explicit request of the IETF which were which observed that there was no security argument for validating the new proposals in 1.3 and so being able to validate something that complies to the letter of 1.3 was perceived as valuable on its own and indeed we could we were inspired by existing papers but we could not apply any existing papers directly to get the security of the standardized record layer so how does it work well the record layer does multiplexing and it multiplexes between multiple keys and multiple sub protocols and so at the top you have multiple sub protocols you are multiplexing their contents using whatever key is available at that time and especially in 1.3 many more keys are introduced so you have intermediate keys for the handshake and you have also a mechanism for ricking so you have to live with this idea that you are going to have a stream of stream of keys a stream of messages exchange on a succession of instances of your authenticated encryption primitives there is also a new format that makes a multiplexing above the encryption and decryption meaning that the content type is read on within the packet and it adds a bit of privacy and also pragmatically it enables the encrypted uncheck to masquerade as an application data which is important for early deployment and so in our implementation we build the top level interface using nested modules that implements a new feature at the time so we have the sequences of multiple strings driven by the handshakes we have the multiplexing of contents within each stream with padding and length hiding then we have a stream encryption with packet numbers then we have an authenticated encryption with additional data and below we have multiplexing on the choice of the prf and the choice of the mac algorithm and that's the last thing i'm going to describe in details in my presentation okay so we are at this level we are going to verify and implement stream encryption for tls so that's the main modules in our implementation for it so that involves some symmetric crypto as well as a few modules for the record layer so i'm going to give you as expected the security definition then outline the constructions the new constructions for tls then obtain concrete security bounds then discuss what you did in terms of verification and what you get in terms of performance so for the definition i don't have a noracle based definition they have a nice picture instead but it's it's equivalent so here we assume the key is established and we model ideal encryption by using this log that is so convenient to reason about using tools like f-star so instead of encrypting we sample ciphertext and we stuff it into the table and for decrypting we just look in the table if that corresponds to something that you want to be for and we return that instead so we switch from red which is the real one to blue that is the ideal one that lets us continue the proof and you want to show what the security loss of doing that for the target constructions so now we look at the standard and luckily there is much less variety in the choice of ad construction than before in fact there is a ccm but it's not used that much and if you look at the others you have a choice between a gcm and chat chat 20 poly 14 or 5 which both have roughly the same use the same construction the same proof structure so in fact our implementation and the proof is mostly shared between the three cipher suits we verify for tls 1.3 and the two cipher suits we verify for tls 1.2 which are slightly different in their what is explicit and what is kept implicit so this is a simplified picture of where it works it's not very surprising so we have a plain text which is arbitrary size so the last block may be truncated we have a prf and we use the first output the the first output of the prf to generate a one-time key that we use to build this the efficient multiplicative mac so at least part of the key has to be used only once for that message and then we put the additional data in front we put the the cipher text next to it we multiply all of that together and we have two final blocks one for the length of the plain text and additional data and one for the authentication tag so in terms of assumptions we rely on a one-time mac assumption so it's like a ufcma but for a single use so we have a variant of our specification that deal with that case and the good news is that we get very strong probabilistic security there is no computer assumptions for that bit for ciphers there is a choice between a yes and chacha 20 and for a yes there are multiple variants and they are we just assume a prf assumption that it is a prf and in the case of a yes we incur the cost of switching from prp to prf so then we write our implementation and we verify it and so what we get is a proof of safety so there is no buffer overrun or privilege escalation just by running your code which is the least to expect we prove functional correctness which meaning that what we are the byte that we output are exactly those matching what is given in the available specification of the algorithm then we prove security by reductions to the prf assumption I mentioned with and we derive concrete bounds by adding the epsilon on paper corresponding to what happens in the code so right now fstart does not enable you to formally reason about concrete probabilities so that the computation of the concrete bound is done on paper on the proof that is structured and verified using your tools so interestingly that involves quite a lot of different proof obligations and so I'm not going to detail of them but I just want to mention a few so as we go down in the stack to build the TLS so at the top as we have seen earlier in my presentation most of the effort is about functional correctness for algorithms like ASR chat chat but there there isn't much to do it just it just shuffles a bit there is a deeper proof relating to a simpler math specs for things like the multiplication in the gawa field for ASGCM and for polynomial and the prime field polyethylene of five so there are there is thousands of lines of implementation revampments of proofs to show that we match the algorithm at the next level most of the proof is about abstracting the details like the lengths and that we don't want to the proofs to depend on for the rest and also about cryptographic agility so TLS has cryptographic agility everywhere so it's and in that case we really want to be able to to prove that there is no bad interaction between different configurations that you made shows and that for example as was the case for TLS 1.2 it's not possible to reuse the same key materials with different algorithms which is at which point solvents are of internal security but here there is no such thing it's actually worked quite nicely then we have the layer of security idealizations where we have two addition steps one for one cm and one for prf and on top of that once we have the ideologue we can reason about how the messages are assembled fragmented reordered and and cut from fragments to blocks and so there is quite a bit to show in terms of injectivity to show that what is authenticated is enough to authenticate the full stream then there are three loops to deal with the fragment loop the block loop and the block loop and the authentication loop for the authenticator from this point the rest of the proof is much more about TLS engineering and has to do with multiplexing by the degree king and also the new feature like zero RTT or 0.5 RTT so as I said you obtain concrete bounds so when that mirrors what was already documented in other papers up to a few details that are specific to TLS 1.3 and because here we just have to idealize module we just have to sum the epsilon there is one thing that is interesting here is that for agcm because there is a 128 bit output of for the block we are there is arguably a chance of collisions as you in case you use agcm with a single key for a very long time and so that was debated a lot on the itf main list in fact we computed that since TLS provides its own RIKI mechanism you can automatically RIKI using what's already in the TLS standard to optimize and get a much nicer controversial bound by just deciding to RIKI every 2 to the 24 records in the rigor layer and RIKI is very lightweight and it's probably important to RIKI even faster than that just to get a bit more forward secrecy for your connections. So as I hope is quite clear at that point this is not just a proof of the design we actually verify the actual implementation that I used to run the demo earlier in the talk and we get reasonable performance it's not as good as the performance from the unit test I have shown earlier so we are still working on it and so for example at the top there is the time it takes to transmit one gigabyte of data and you can see where we are right now so we used to have OCaml as a backend instead of C and OCaml is a high level language which is very bad at byte level manipulations and so you can see that we lose several orders of many to just using your high level language instead of C and the optimized algorithms in C so that's that's done that was a very important step so this compares all implementation integrated with the proof together with using OpenSSL and you can see we are still a bit slower but I expect most of the discrepancy to disappear once we integrate better the latest verified algorithm from tools like fail to or verified security stack so for example we are now at just eight cycles per byte for implementation using a portable implementation using yacle star which is a bit better than OpenSSL at least until you start using xc for optimized much faster implementations so there is also verification cost so that that proves wasn't easy in particular because it goes down to every detail to be standard compliant and but it's very modular and reusable so we can build upon it and it's very easy to add variants or variations of it you can see that the proof consists of putting explicit specification and auditions that get erased as we compile to C and so but because we also use metaprogramming to do inlining and to specialize the code in C in fact we erase the proof between line and diva and express what you do in a lower level language so the the the size of the code before and after compilations are not that different oops sorry about that so in term of time so that's not the manual verification time it took us a few months to get there and to get everything in place but once everything is in place this is the time it takes to verify as part of continuous integration so every night we check that the differences in producing the tool don't break the proofs that you already have and it's at that point it was a bit below two hours now it's more like one hour but it varies on a daily basis and so we are putting a lot of engineering effort to maintain our proof and to make sure we don't break things as we improve on that feature both the protocol and to the language but that's that's quite a significant engineering effort to to get there and then to maintain it on an ongoing basis at the same time provided we get that ongoing we can make a change and two hours later you have a full verification again and in fact most of the proof can be factored out because each module is verified completely independently so it's it's not that bad from that viewpoint all right so time to conclude so so in this talk I presented what you are trying to do with HTTPS we think it's okay we know it's quite complex and critical but you also think that it's small enough to be in range of cryptographic verification at at the level of details that gets into the standards I did not mention much related work or colleagues as part of this talk but as should be obvious by now this relies on a very deep collaboration between cryptographers system researchers programming language researchers and verification specialists and that's that's quite a lot of fun we also have new tools I said very little about the tools themselves but we have interactive tutorials we have papers there are lots of details out there if you want to check them out and I hope I have convinced you that we have a method to get a safe functional darkness and cryptographic security for a useful standard compliant system code so here are some pointers so the code is the code and the papers everything is available online in particular if you go to a salon you will have lots of tutorials including some cryptographic tutorials explaining what it means to use the tool and giving you a way to start with the tools if you are curious okay well thanks


I think what's important to realize is that as brands we need to move from creating communication to creating content and that requires a slightly different mindset. It's not the same as creating communication strategy. Communication means as a brand when you're speaking to consumers. Content means you're creating content for the love of entertainment, engagement and by the way the brand is part of it and therefore that's one part. The second part is the authenticity of what the brand stands for that needs to reflect in the content. So it's not about creating content to sell only but creating content that brings the values and what the brand stands for. So in that sense if you call that a strategy, yes every brand needs a content strategy and bring that to life. What it means is firstly you need to have a very strong and powerful brand that you can translate. If you look at most of the content that we are consuming today is really really well thought out and strategized. If you look at for example say I was talking about it earlier, the Marvel Avengers series. I mean if you look at their content strategy they've been working on it for the last seven eight years and they've got us hooked. It's very very planned and deliberate. So that kind of thinking is what you need but again comes consumer out, comes reflecting your brand philosophy and not necessarily with the intent to communicate and to sell. I think it's from a brand point of I think two ways perhaps. I think the first thing is whether the content is being watched and loved. And I think that is probably the first KPI, how much it is being watched, how much is it being loved and how much is it being shared. The second of course over a period of time and again not in short term because I think it's difficult to perhaps measure brand KPIs in the short term for content but over a period of time is your brand love, is your brand affinity, whatever your brand metrics are they growing over a period of time if you're constantly engaging with the content. But again big word there is not to look at it in the short term but look at it in the long term over a period of time.


What is the Activity Chooser? To use Moodle's Activity Chooser, enable Edit Mode top right, click where you see the plus sign anywhere on the course page or click Add an Activity or Resource. This will bring up the Activity Chooser. Depending on your administrator's settings, you might see an All tab which displays every type of learning content available to use and or you might see two separate tabs. Activities, these require students to interact with Moodle such as posting in forums or submitting assignments and resources which students read, watch or listen to. The icons are colour coded relating to their function Green for communication Pink for assessment Blue for content and Red for collaboration. You add an Activity or Resource by clicking it to go to its setup page or you can click the information icon to find out more and then click the Add button bottom right. You can favourite an item by clicking the star and then easily find it again from the starred tab. Some administrators recommend activities and resources they think you'll find useful. As we can see here on another Moodle site where the admin has recommended three activities. Again, this is to help you locate them quickly and encourage you to try them. You should also see a link to MoodleNet at the bottom of the Activity Chooser allowing you to browse Moodle's site for finding, sharing and curating open educational resources.


So in order to do calculus, we need to be able to find limits, and so let's start with multivariable limits, and let's keep in mind a limit must be the same no matter how you approach the limit. And as we saw, this can lead to problems when we have two or more variables. So let's think about this. The problem we ran into is that we let x, y go to zero any way it wanted to, and we are able to get different limits depending on how x, y went to zero. So maybe we can restrict how x, y is going to go to our point. And here's where we have to be a little bit careful. Once we do that, we are limiting the calculus we develop to certain types of functions. The good news is the types of functions we can apply our calculus to include pretty much everything you're familiar with. So far you've studied single variable calculus. That's the calculus of functions using one variable, like y equals x squared minus 4x plus seven. Wait a minute, aren't those two variables? So let's talk a little bit more about those variables. So remember a function takes inputs to produce a unique output. So the area of a circle is a function of its radius, and here we have one input, the radius, and so this is a one variable function. Or the area of a rectangle is a function of its length and its width, and so here we have two inputs, and so this is a two variable function. Or the votes of a politician are a function of their corporate sponsors, and here we have several inputs and we have a several variable function. So rather than letting x, y go to zero, zero at the same time, let's break it up. Let's find the limit as x goes to zero of the limit as y goes to zero of our expression. Now parentheses still mean the same thing they've always meant. Take care of the stuff inside first. So to find the limit as y goes to zero of this expression we'll let y go to zero. But what's happening to x? And at this point we can invoke a time on a tradition, procrastination. And in this case since we know nothing about what happens to x, leave it alone. So we want to find this limit, well x will leave as x, and y will let go to zero, and simplify. And so this limit as y goes to zero is one-third. And now we want to find the limit as x goes to zero of one-third, which is just going to be one-third. Well let's switch the order of the limit. So let's find the limit as y goes to zero of the limit as x goes to zero of the same mess. Well since the limit as x goes to zero of the limit of y goes to zero is one-third, then if I switch the limit around it's got to be the same thing, right? Well you're probably not taking multivariable calculus because you're bored and need something to do on a weekday night. Chances are somebody is going to do something with the problems that you solve. And here is the most important thing to keep in mind. If you don't find the flaws in your work, someone else will. So you really want to be careful about making statements like this without knowing that they are in fact true. Because if they're not true, somebody else will tell you that they are false. So let's check it out. So again, parentheses say do the stuff inside first. So we'll find the limit as x goes to zero of this expression. And again, since we know nothing about what happens to y, we'll leave it alone and get a limit of one-half. And then our limit of one-half will be one-half. And this problem illustrates a key point. Don't switch limit processes. What that means, a limit process is anything that involves a limit. These are things like, well, limits of course. Derivatives, don't forget that the derivative is defined in terms of a limit as is the integral and so are infinite series. And the important idea here is that if I have two limiting processes, for example, the limit of an integral, I can't generally switch them to be the integral of a limit. And if I do, I can't guarantee that they're going to be equal or in fact have anything to do with one another. And this is an important idea to keep in mind because you're about to have a bunch more limiting processes available to you.


What does inner balance mean to you, Sai Guru? The inner balance will only happen when you determine what your thoughts and emotions will be. Somebody can say pretty things to you or somebody could abuse you. But will they decide what happens within you? What happens around you? You can never determine a hundred percent.  To some extent, if you have fifty-one percent control, that means you have the controlling stake. Hundred percent if you ever have. Tom is giving up. Me too. It's okay, because I have a good... The one who has fifty-one percent is pretty good, so I allow her to make all the decisions. What is around us never happens hundred percent our way. But what's within us, our thought, our emotion, our body, our energies, must happen the way I want it.


Yes, they have been upweld. No, no, no, no, no, especially when you ride the two people, when you go at the people. Kazen, when we come back here, I think it's better than Kuni. Hehehehe No, to such a mix, Tanzania, to Tanzania and the DRC. No, to such a mix, Tanzania and the DRC. Yes, yes, Kazen. We take you to another constituent. You can see that in the background there those that are watching us from across the borders of Zambia is all about our smiles. And let's find out in terms of what the outcomes are. And we will begin with Honorable Stephen Campion, who appears to be the chief whip actually in parliament, just to ash us into of course the celebration that we are seeing in the background. Honorable, please take us into this celebration that we are in again today. Yesterday the people of Zambia were subjected to a celebration. Where are we this morning? Thank you so much, Comrade Pili, and we are grateful for you to be with us this morning. Yes, indeed. We have had mixed feelings. Of course, you know, it doesn't please us when we hear the few seats that have been notified through the courts, but we do respect the due process of the law, the justice system. Today we are filled with joy, of course, because we had two matters that had come up for judgment. The first one is for our dear lady here, Honorable Mourin Mavonga of Ufua constituency. Whose erection have been upheld? She appeared before Judge Monsa and she has been cleared because she was petitioned by the UPND losing candidate. One of our elder brothers who has been around before, who had saved the people of Ufua before, but of course he had nothing to show. And the people said, look, we have had you, but I don't know what he thought he could achieve in the courts of law. The same UPND agenda, but we are happy that the courts have upheld the erection of our dear sister here and we thank the people of Ufua and all the leadership of Ufua for the work they have done. Similarly, we had a matter before Judge, I think it should have been Judge Nkonde, in respect of Honorable Mungando, who is also a provincial chairperson from Chinga, whose petition has equally been thrown out and we are happy. In fact, for them, the petitioners have been condemned with costs so that they don't waste the people's time and the costs change. So as a PF whip, I'm really happy and grateful that now these members of parliament will get back to work. People elected them to do work and we would want to see that, look, even as we are here, my colleagues, we are happy also we have got the Honorable MP for Lukasha, who is here, not as Honorable MP, but he is here as our senior lawyer. He was also representing me, leading the team that represented me in my petition. His judgment was also two days ago, which was also equally upheld in Lukasha. So we have got so many problems to deal with for our people. As we speak to you, our people whose measures have been sold to FRIA have not been paid, which never used to be the case. True. As we speak to you now, we don't know where the fertilizer, the number of bags of fertilizer which our people used to get here have reduced. We don't know whether they are now trying to say, because we had them talking about balancing, giving a narrative which is not true, that PF was segregative in terms of distributing inputs. So if they are trying to show that they will take the bags that they have grabbed for our people to the southern province or other regions, they are really just fighting this country. And they must stop because the food that is grown here does not only feed the people in Muchinga, does not only feed the people in northern province, it feeds the people across the country. We will know that we had droughts two years ago, southern western province. There was no food. Where was the food coming from to go and feed people there? So let's not be narrow in terms of the way we want to manage the state affairs. We are saying, you knew donning. I don't know if it's new down. Get to work for the people of Zambia, regardless of where they are. Yeah, that's where we grow more food, we have granted rainfall. So if you start subtracting from the farmers where rainfall is granted, the soils are fatal, what are you doing? As we speak to you now, I think people expecting 250 kwacha, bag of fertilizer. Now we have reduced. How are they going to buy a bag of fertilizer, 880 kwacha? We saw people moving with plastics of cooking oil. The president moving with plastics. The prices here are still going up. And to the slogan, the only thing we are seeing going forward is dollar against kwacha, which was supposed to drop from mid morning for the sunset of being inaugurated. Now we are saying this is what the government should focus on. And I was shocked to hear my colleague who I respect so much, the minister for local government and rural development, wondering where the MMPs were in the chamber of parliament. What kind of hypocrisy is that? Here we are. How many are we? Right here we are three. The other colleague is just in the other courts. The other one will be in the court tomorrow. And our colleagues in other areas Kasama and in northern province, Ruapula, it's the same. So when you say we are the members, I'm speaking alone, you should know. Your president was in the same parliament telling the nation that no, we were not going to go into petitions. Where are we? Because we could have been in parliament doing, representing our people. So this is the leadership that we have here, which is referring to understand that they are now governed. Don't point to us. Asa here to check that your promises are fulfilled. You can't continue saying no, this one didn't. No! When you take over the diving of the viejo, you don't point to the previous driver. It's you. When you prank the viejo and they ditch, it's you they are going to say you were driving at the time of an accident. So the country needs leadership. So not focusing on wrong things. You can arrest Mr. Chama and keep him for 20 days. It won't bring down the bag of minimum, which is supposed to be a 50 watt. It won't. Now we are being told fuel is going to be increased. What we were told before elections, we were going to move the middumen because we were accused of having middumen in the supply chain of fuel. Now today it's a different story. We want to hear the people, the person who promised the people of Zamderati fuel was going to be single digit. That's what people are waiting for. Electricity was going to be cheaper than what we were doing ourselves after investing so much into electricity. So these are the issues we shall hold them accountable. Andji, because of the people, we are here. And we thank the judiciary for educating on our matters. Yes, we have got concerns but we still know that the judiciary has got further channels that can be exhausted when we feel aggrieved in terms of the decisions that are made. And that's what we are going to pursue. We are never going to cast suspensions on the judiciary at all because we respect them. And we know that it's one institution with capable men and women who cannot be intimidated, who are able to decide matters as they see them through the law. So that's where we are Mr. Piri. And to those of our colleagues whose decisions were not positive, please like I've said, let's not cast suspensions on the judiciary. We shall follow the processes in order to have these matters looked at.


Top three tips to pass the TikTok interview. Number one, you must understand the future features you're going to work on at TikTok. For example, in my last video, I mentioned TikTok shops hiring aggressively. You must understand and use the TikTok shops and imagine what the future challenges for you to grow the user adoption of TikTok shop and spend more money on TikTok shop. Number two, create a product portfolio to demonstrate your future features you want to create for TikTok. This really includes the end-to-end thinking process. It's going to help you think really hard so you can prepare it to be better when you build your portfolio and impress hypermanager when you show your portfolio as well. Number three, use your latest interview question database to practice. They're going to ask you questions like this. Is Instagram shop successful or not? How would VR new technology impact TikTok? Like and save this video for upcoming TikTok.


Hi and welcome to the session. The question says, in a hot water heating system there is a cylindrical pipe of length 28 meters in diameter 5 centimeters. Find the total radiating surface in the system. Let us now start with the solution. Now here we are given the length of pipe that is denoted by h is equal to 28 meters and this is equal to 28 into 100 centimeters since 1 meter is equal to 100 centimeters therefore changing 28 meters into centimeters this gives 2800 centimeters. Also we are given the diameter of the pipe is equal to 5 centimeters therefore radius of pipe as denoted by small r is equal to 5 upon 2 centimeters. Now we have to find the total radiating surface in the system and that will be equal to the surface area of the cylindrical pipe. So we have to find the surface area of the cylindrical pipe. Now the formula to calculate the curved surface area of a cylinder is 2 pi r h. So here the curved surface area of the pipe is equal to 2 pi r h where r is the radius of the pipe and h is the length of the pipe. So 2 into 22 upon 7 into r is 2800 centimeters into h is 2800 centimeters sorry and r is 5 upon 2 centimeters. So the curved surface area is in square centimeters and simplifying this we get 7 into 4 is 28, 2 0s, 2 cancels out with 2. So we have 22 into 400 into 5 centimeters square and this is further equal to 4400 centimeters square and since 1 centimeter is equal to 1 upon 100 meters therefore 1 centimeter square is equal to 1 upon 10000 meters square. So this gives 44000 divided by 10000 meters square and this is equal to 4.4 meters square and hence our answer is the total radiating surface in the system is 4.4 meters square. So this completes the session by intake care.


Almost time for the bell, how many options will you sell? Fire up your platform, get ready to enter But first let's get the mindset centered Hey, hey, let's go We're not here to gamble, we're here to trade We follow the plan, that's how we get paid Test and trade it, have success Find what works for you and forget the rest Stats and probabilities is what we're about Time to dismiss greed and doubt Focus on the process, not the money And the profits will flow like honey Power our lives, let's start the show Come on trade hackers, get ready to go Zero-day options, time to make bank Get locked and loaded, then be ready to plank Hey! Which hit 30% and was out Oh, no, that's not true I did some discretionary puts I got stopped out on those On that little flush So, here we are for power hour Looking like a five-wide strangle Is in order S&P up 29, NASDAQ up 104 Russell the strongest up 26 Dow up 163 Gold and silver a little bit green Notes and bonds mixed Oil off about a half percent Natty gas up about a half percent Grains a little mixed, Euro and the pound A little green Bitcoin 27,000 and VIX Down about 5% hovering just under 17 Gonna buy some longs here Oh, we are on a short squeeze, aren't we? Yes, we are. All right, so I'm doing two to one All right, got my longs in place Yeah, it looks like the 65-60s Give it a couple minutes Yeah, I've got the move at 0.55% right now It's kind of hovering above the expected move for the day See if we are going to stay above that Now I'm seeing less than 0.5% As we are coming down I've got about a minute here Let's see what this does Mario you are going one to one because it makes a big difference I haven't checked the back test Yeah, we are going definitely under now All right, I'm going to go one to one as well Are we going to get 10 wide here? Looks like 10 wide Trunch one, 10 wide, 10 lot I'm going to get filled at 0.655 Let me just drop it quick on me And I got filled at 0.625 I don't like that But I'm in All right, so low premium Trunch one But is what it is I got in the 0.65 and 0.55 It kind of moved right before I entered So if you got in right after the 0.5 till You are probably 5 wide And ourselves a little sell off here Just giving back over Over half the gains on the day At an SPX high of day at 43.85 Back to 43.57 How's that treating the old Double calendars here, let's see SPX one still down My NDX Single calendars Pretty break even My 1.2 is up 400, 500 bucks from this morning My 1.3 is up about 180 I did those with CPI and PPI coming up I did those a little bit bigger today So I'm going to shed some of it Towards the end of today Going into CPI tomorrow morning pre-market And what else did I do I did some time fly adjusting With this little pullback That still needed to be adjusted That one did the other one Let's open that one a little bit Took off a QQQ duck For beak profit I saw some of you guys took off your SPX one I was looking at that as well Let's see where we're at now It's right down the edge I'll leave it for now Got a rut duck that expires at the end of this week Got a chance at a duck head If it comes down a little bit That oil premium is staying bid Our VXX verticals came in nicely With the ball contraction So on the November one If we get the VXX gets down to about Call it Below 21.5 bucks We should hit our profit target on that one On the October one Needs to get down to about About the same So VXX gets under 21.5 I'll start to Peel some of those off So one of the FOMC members Speaking today, is that what happened? Kashkari, say something stupid No, he speaks it He just started speaking Remember Waller spoke at noon? Yep, that looks like what did it Right at noon, central Oh, Bostick, I have Waller On my calendar Same guy, I can't tell the difference They look alike Testing the waters Seeing what the market does Based on different things they say Who knows, could have been Just a little profit taking as well We always want to think That there's a reason for a little price movement But there's not always Oh yeah, it's planned, no doubt Alright, Bostick, you say this Waller, you say this Kashkari, you say this Let's see how the public and the markets react That way We go to do our meeting We know exactly what we need to say See, what else we got going on here? Yeah Then they get on What's that, betting site Where you can bet on economic things Wouldn't doubt it Yeah, predict it Predictit.org You can, I think you can bet on Politics and economic stuff Oh, Dick K, are you on here? I was going to I was going to look at your I was going to compare that trunch one you sent me To mine, I haven't had a chance today So I figured I'd do it during power hour If you're down with that Yeah, I'm getting some nice Dick K here so far Dick K, Colin Dick K No Dick K today He's in here, I see him in Zoom He must have me on mute Wait Share the meme Post the Dick K meme Maybe I'll do it after trunch three Yeah, he may need your accounting services for that Too many ones to carry And zeros to Too many zeros and commas And ones to carry Yeah, he's going to need your help So we're still hovering We're at .49% now I don't, I only do it on trunch one But Marthenis is at for trunch two It looks like See what you got Move up half percent Monday, Tuesday, Wednesday, Thursday, Friday Stop six Up to three Solid I'm going to put that in my coffer for next month Two Short Marthenis style Cool, thanks for sharing Got that on my next month To-do list Six twenty-five Let me check your math, Krish Since You know, like I said yesterday I can't really trust you 3.75 See I knew I had to check on you My Missing the Stop production Yesterday helped me, though Thank goodness I didn't believe you yesterday, Krish It's always good to be lucky sometimes, you know Sometimes we get unlucky slippage Unlucky things happen, so you know You gotta take advantage of the luck on your side sometimes, too That is the only reason I didn't get stopped Yes, it is Because I did not reduce my stop Because I was Yapping away and Didn't see it Hit the level and then Krish told me that it did But I didn't believe him So thanks to you, Krish That was my biggest power hour ever yesterday So, Tronch 1 is down to 4.40 I'm looking for 3.75 Almost time for Tronch 2 Look how close these calls are The 5 cent calls Getting close to price Let's see, I already bought some extra puts here, so We got 20 puts, so I just So I got 10 So I got 10 puts, I just need 6 A lot of blackout dates I had a I better note that So basically, Marthenis, you went through it And any time there was a Losing trade, you just added that as a blackout date So that would happen Thought that looked pretty good for Tronch 2 I've looked at that before, that would look really good Alright, so We're looking at 65-60s Tronch 2, 5 wide 5.95 65-60s So I'll look for 3.60 Tronch 2 to reduce stop Yeah, still looks good Vegas Michelle Vegas Michelle, how's the Football betting going this year? Nobody wants to talk to me today Vegas Michelle, shunning me Dick K, shunning me Oh, Dick's back, alright He just had me on mute for a while I am, I'm very sensitive, Dick You know that I was just saying, I I haven't had a chance to look at that Tronch 1 In detail yet, but I was going to do it here After we get done with Tronch 3 Yeah, it looks solid Just the brief minute That I had to look at it Well, I'm kind of a slow Kind of slow, Maro Tronch 1 is down to 3.80, getting close I'm looking for 3.75 I'm only at 3.95 4 MRP says 3.7 I don't believe them I don't believe that MRP Chris, now Chris is agreeing I definitely don't believe it 3.90, 3.75 Okay, there it is Reducing stop on Tronch 1 Tronch 2, I'm looking for 3.60 And it's currently trading at 5.10 I just, I got to see it with my own eyes I just got to see it with my own eyes It's just how I am Yeah, on Tronch 2, I got No, 5 wide, 65.60 10 wide on Tronch 1 5 wide on Tronch 2 It's falling asleep on the expected move line Let's just ride that into the close Tronch 3 Find some longs Maybe 10 wide 65.55 Couple minutes Now we're looking like 5 wide Give it another minute Could be the 65.55 Alright 65.55 Tronch 3 10 wide Try to get filled at 3.10 Got one contract filled at 3.15 And the rest filled at 3.10 65.55 Thursday is the new Wednesday, Dick You didn't know that? You didn't hear? Thursday is going to make it come back Alright, so Tronch 2 is at 4.40 I need 3.60 Yeah, so Dark Avenger You may want to... I was chatting with somebody yesterday They're using XSP And they are Claiming that the Fills, not Paper trade, but actually trading XSP real Which is obviously a tenth the size of SPX Good thing to practice with But they were saying at the end of the day The liquidity is pretty good So I said she was not using stops though She was just Manually Monitoring and closing I don't know how the stops Would be on XSP I can't imagine good So for Tronch 2 Who's in the 43.60s And 65s for Tronch 2 That can Notify me if that gets down to 3.60 Anyone but Krish Alright Can you let me know when that gets down to 3.60 I want to I want to check out this Tronch 1 That Dick K sent me Okay, so a couple things that I did, Dick I added Thursday back in Because I love Thursdays What else did I do? I think that's it So if I go to mine Alright, so Make sure I got everything kind of apples to apples here Starting capitals the same 10 contracts Okay, so I remember the win rate was quite a bit higher So it's 69% win rate versus 57 My mark 23 versus 24 Drawdown Minus 5 versus minus 5 So about the same P and L About the same But the big thing is You're getting out of a third of your position At 40% So you're taking a bunch of risk off the table To me That's The win rate and Taking those chips off the table like that And still beating the other one That's attractive to me Risk off, exactly I didn't check the blackout dates Is that just FOMC? So if we take out Thursday So we got 69% 24 minus 5 69, 24 minus 5 20 minus 5, 0.7 No, sir, Thursday stays I love Thursdays Thursdays, it's got a bad reputation But it's a good guy You know, it's a good guy More profit, more mar Less drawdown, I mean What's there not to love about Thursday on this one? Add that to my Next month's cheat For Sharon Dickay Trading at 390, I need 360 If I do the opposite, if I take away everything Except for Thursday Oh, that's the other I knew I changed something else I'm looking at it for Going back to May 2nd I still look at them Going back to that date That's the difference I definitely pay attention to Here to date But I still use May That's it Okay, 390 85 360 I'm a big fan of nostalgia 375 380 375 Pretty well centered here for Trunch, too But not quite getting it Tiny push-up The Germanic God of Thunder Thursday's powerful There's no doubt 370, 365 I'm going to close Here pretty soon, I'm going to close 7 of 10 On my 1, 2, and I'm going to close 3 of 5 on my 1, 3 I just want to have a small position and go Into CPI tomorrow Still haven't quite got to 360 yet Need a little 2-point bounce Now that's going to take a few Days to work itself out, I think Tomorrow I'm planning to stay into that Until Monday if Assuming we are in Decent range and I don't have to close For To manage risk Alright, I saw 365 There we go Reducing stop on Trunch, too There's that little 2-point bounce Alright, so Between 1665 21 minutes to go Anytime we can be in between Pock and VWAP You know we're in good shape We'll see where we are here in about 15 minutes Alright, I'm going to try to close Some of my BNBs No fill at $12 No fill at $11.95 Got filled at $11.95 The 1, 3 I'm going to close 3 of 5 I'll try to get it filled at 18, 20 No fill at 18, 10 Oh, filled at 18, 10 Alright, just posted those exits in the calendar channel I did spend about 3 hours doing some Calendar back testing last night I've got a few little tweaks, nothing major Just a few little tweaks For next month It's more doing I found, I just found a little bit of value Doing Not necessarily just doing 20 delta Or 25, you know some doing like 15 delta on the call side 20 on the puts Some as much as like 15 on one side 25 on the other And then I'm Trying to remember Start trading more 2, 4s 3, 4 I was looking at a ratio on a 3, 4 Doing like 4 to 3 3 puts to 4 calls On Mondays Added a 1, 4 Yeah, that is interesting, Nick You know what, I I may dig into that as well For all my zero DTE now Pretty much, except for the Yes, I've kind of switched over to Fixed premiums But I'm still Deltas on Calendars, but What do you got here So this is the Mini B&B 1, 3 Monday Tuesday 20 dollars Versus Starting capital 100 Text per trade Yeah, definitely a nice improvement Open trades at 3pm Versus I'm open at noon I'm closing them at the open the next morning So are you You have a stop loss Which I don't know if that's Really relevant since you're just holding Overnight and closing in the morning But I'm going to note that I got a lot of homework today, you guys are giving me a lot of stuff to do today All right, good deal A lot of good stuff going on today But you don't actually Put on a stop loss overnight on Calendars, do you Nick? I would I would highly suggest not to do that You just makes you feel more comfortable Just makes you just comfort to you on the back test 10 minutes to go Yeah, I'm not a fan of using a stop On any kind of option trade Overnight Man, this thing's just Sleeping on that Expected move here Going all the way back until 10 afternoon No wiki wiki So the API only gives SPX on Delayed data Hmm Yeah, that can't be good Trunch 3 is down below a buck Trunch 1 is down below a buck I have my order at 60 cents I'm going to leave it Hugging my lower strike 35 I'm going to take that one to the bell Put that at 10 cents Trunch 3 is the 65-55s as well Put that down to 10 cents Trunch 1 is trading at $2.30 That's the 65-60s I'm going to get out of that one Give it another minute or so Who woke the dragon?  Filled at $0.30 on Trunch 1 $0.78 Trunch 1 I got in at $0.625 Wow, I got filled at $0.10 Didn't let me take it to the bell So I got into Trunch 3 at $0.3 $0.3 $0.14 $0.4200 So I got $0.4200 $0.4320 $0.590 $0.590 Equals $0.144.70 $0.144.70 $0.590 Minus the cost of my $0.5 longs Nice Nice, Elliott Over $0.17K Beautiful Back-to-back Back-to-back big power hours Back-to-back big days overall Good stuff Alright my friends We got live stream Tomorrow morning In the morning session On what is tomorrow October 11 Wednesday And then We'll be doing power hour Back here Same bat channel Same bat time Good night everyone Take care


Hello. Welcome to the first of two e-lectures about writing, where this one deals with the evolution of writing and the second with a classification of modern writing systems. Writing is defined as a set of specified visible or tactile signs or symbols representing the utterances of a language. Without writing, our world as we know it today would certainly not exist. Among the most important prerequisites for a set of signs to be classified as a writing system is the existence of a language with a set of rules and conventions that is grammar shared and understood by a group of people. The next step is to preserve certain ideas or facts for a specific reason. That is, we need contracts, lists, religious motives, etc. And subsequently, a set of signs or symbols has to be developed that is able to represent the basic elements of speech along with a convention as to how to order these elements accordingly. Finally, a form of a distinct representation on a medium for the developed system needs to be chosen in order to store and interpret the signs. In contrast to a writing system that is always linked to a specific language, other signs, paintings, icons, street signs, maps used for communication do not necessarily depend on the prior knowledge of a language in order to be understood. Mathematical symbols, for example, convey an abstract idea rather than a set utterance. Thus, the symbol for the number 8 can be pronounced in many different languages but still retains the exact same semantic value. Writing did not appear from scratch. A long, evolution process proceeded before a set of signs could be called a system. At some point in the past, our ancestors felt the need to preserve certain information. Paintings done some 17,000 years ago depicting hunting scenes and animals of the time are the first documents our forefathers left behind for others to see. Lascaux is the setting of a complex of caves. In southwestern France, famous for its paleolithic cave paintings.  They primarily consist of realistic images of large animals, most of which are known from fossil evidence to have lived in the area at the time. Altamira is a cave in Spain, famous for its upper paleolithic cave paintings featuring drawings and polychrome rock paintings of wild mammals and human hands. The world's famous feature of this cave is found on the ceiling. Coloured paintings, mainly from the beginning of the Magdalena period about 15,000 years ago. Most paintings show bison, but there are also other animals and some other figures in a simpler style. The development from then on can be subdivided into three phases, proto-writing, early writing and modern writing. Let's look at proto-writing first. Long before true writing came into existence, people in all parts of the world already used sets of signs to convey meaning. Memory aids or mnemonic devices were used to keep track of obligations for accounting purposes and many other listings. However, no linguistic units are connected to the marks applied, hence they cannot be seen as writing proper. Here are three of the best known examples. Tullies or tally sticks, for example, were bones or sticks with notches carved on their surfaces. They were used virtually all around the world for record keeping and to document numbers and quantities. Or take the kipu, a recording device used in the Inca Empire between 1300 and 1600 BC. It consists of a series of knotted strings joined together on a cord. The knots were encoded in the decimal system and were used to record tax accounts, astrological notations, mathematical operations and other numerical recordings, for example dates. Well, and then here are the Sumerian clay tokens, small, differently shaped clay objects that have been found all over the Middle East. It has been suggested that specific shapes were connected to specific entities such as numbers or everyday objects or both. One specific token for 10 sheep, for example. Clay tokens thus could have been used for record keeping and accounting. Systems of this kind were in use long before and often also alongside writing and mainly served as reminders and controlling devices. But what about real writing? New findings suggest the beginning of script was in Transylvania in Romania. Several sets of signs found imprinted on clay tablets are associated with the new civilizations that lived in Tataria and created these tablets in about 5300 BC. But although 200 and more signs have been found, it is not clear if the set can be classified as a writing system. No recurring sequences of signs have yet been identified. The discovery, by the way, caused great interest in the archaeological world as it predated the first Minoan writing, the oldest known writing in Europe. Later on in the Sumerian Empire, around 4000 BC, people began to develop the first acknowledged true writing system, the so-called cuneiform. This script is one of the earliest known forms of written expression. Emerging in Sumer around 3000 BC with predecessors reaching into the late 4th millennium, cuneiform writing began as a system of pictographs. In the course of the 3rd millennium BC, the pictorial representations became simplified and more abstract. Cuneiform documents were written on clay tablets by means of a blunt read for a stylus. The impressions left by the stylus were wedge-shaped, thus giving rise to the name cuneiform, wedge-shaped from Latin cuneos, meaning wedge. Writing was done on a clay with a special triangular-shaped pen. The symbols were pressed into the wet clay surface, then dried in the sun or baked for preservation. Often these early writings were contracts, or they were done for record keeping. Eventually a number of different writing systems appeared all over the world. Many of them are clearly related to one another, since great cultural achievements of one culture were often recognized as extremely useful, for example, by neighboring states or conquering armies. Today, less than 15% of all 7000 attested languages have writing systems, and not all writing systems encode information in the same way. Modern writing systems can be divided into two central branches. There are logographic writing systems, which make use of symbols that represent words or concepts, where the shape of the symbol employed is often closely related to the meaning of the respective concept. And there are phonographic writing systems that establish some sort of relationship between the written symbol and its pronunciation. Both modern writing systems have several variants, which I will introduce in a follow-up e-lecture entitled Modern Writing Systems. Until then, have a nice time and thanks for your attention.


Good morning cyber traders. Happy Friday everybody on this 15th of November How's everybody doing good to see you all Lawrence Michael Grant could see you all Brian everybody all you cyber traders everybody ready for the weekend And the cold is kicking in so far. I don't know about where you are but reason over here in New York, but anyway on today's Friday, we know what to expect and Couple of stocks move this morning when I talk about them. Some got to shroy We're gonna talk about this TR OC That was a classic and we're gonna talk about some other ones We got that JC pennies and everything else a lot of moving stocks But we can also let let's go over and see what's going on for today What happened yesterday and then we'll go through what's moving this morning first of all a couple of nice little moving stocks yesterday We had the Cisco trade yesterday That stock of earnings came out it really not going anywhere You know when you could see the point of that you could see we're from 48 down to 44 You look here in the long-term chart was a pretty decent short time frame doesn't look that good There you go right there That was actually a little bit more of a brand name stock not really my forte You know, uh, it's some of those some other stocks that were a lot better And it basically got crushed Third day in a row DGC I Mean this thing is just like just pouring it and pouring it down just literally getting crushed What a nice little stock right there, too, and you know short Everywhere look at it's testing. It's testing the lows. I'm putting this back on the watch list You know sometimes we trade stocks from the day before Till the following day because sometimes they keep trickling down That's how we find day trades to become swing trades. My best trade yesterday was the C. LVS I know a lot of you guys got on that trade right there that stock Just literally had a great great pop right in the middle of the day. It just literally just went from a 620 all the way to 660 that one was a really really nice one IGT Another great mover. That's actually a lot prettier. The only thing I didn't like about IGT is it got some once in a while. I had some really really ugly Spreads and that was about it But other than that everything else kind of worked out pretty well, so everybody did pretty well yesterday Oh, we had the peat on that was pretty cool, and what was the other one that we had? I'm drawing a blank and very remember what else we had. We had another stock that was pretty good yesterday We had that one Uh Not at that which one was it it was one more stock that we did pretty well on I'm trying to think there's just so many of them that We traded yesterday Unfortunately a lot of them moved in the middle of the day Was the CRZO is that what it was? That was a nice short right there now the AMR and the AMR and is moving now and I mean I had a big move You know the day two days before it's moving again right now But that's basically what we have All right, so let's go talk about what's moving today Because there are a couple of good stocks that are moving this morning now regarding about what we're trading Listen, I took listen. I'm gonna be honest with you I took two losses this morning already and let me tell you something. I broke my 32nd rule The stocks didn't go my way I took a very very small loss and thank God I got out of them because if I didn't I would have lost Probably three times more than what I did and let's talk about them really quick You know, I'm a big bottom fisher, okay, and I love bottom fishing and that's not talking about the fish in general just like I love stocks to get crushed and This stock right here has just been getting Literally destroyed last couple of days. You could see it had a nice little rally went to 10 look where it is A buck 70 now. Let me just change it change this view right here All right, so I had this stock. I was hovering right around $2 and I I averaged down I bought a little bit more at a buck 95 and then and then it really just dropped to a lot of buck Buck 87 and it was like, you know what things not going my way went back that back to 2 I was trading it right around 815. I know a lot of his jumped in around 8 o'clock. We saw a nice little run I you know, sometimes when these stocks get this Decimated they don't really come back So I thought it was coming back when I looked at around 830 and it didn't and I got out of it and good thing We did because look where it is at a buck 60 and the other one that almost got me was the JC penny I Know grant we were talking about it earlier when he's grant sister. That was a good call fast on the grant Well, you know what I said I had support levels at 30 and a buck 30 I'm like, you know, it's not really breaking it and You know another one I bought it at 31 It was hovering at 30 and then I saw a big buyer get executed at 30 and I went to 29 I got out of 29 and got out of it and once again look where it ends. So remember You know, even though being your mentor and being here in trading you kind of understand something You don't win every trade. Okay, you don't win every trade and you know Everybody always likes to talk about the winners The funny part is nobody likes to talk about losers. Alright, so here I want everybody to know in the cyber group room We do lose money, you know, I mean you see him like Jerry just made 26 cents in AMR N Benito just made a 45 cents in AMR and that's great. You know, but we also lose So if and the big thing is just like you're in class yesterday, you know, how you learn how to trade Losing money, that's how you learn you learn from losing. You know why? Because if you know why you did it, you're not going to do it again That's how trading works. So you can't always think that every trade you make you're going to win. So anyway, that's that's one of the lessons that hopefully a lot of you learned in the pre-market And you know, this pretty pretty normal, you know, pretty normal as in on a Friday, you know, not the greatest days, remember Tuesdays Wednesdays and Thursdays is always the best days of trade Now let's talk about what's moving in the market. Let me give you the watch list that I found. First of all, we had this AIHS stock has been on a huge run up and big, big mover. It's up 169% right now. Very, very cheap stock. Unfortunately, my broker won't let me trade it. It breaks the 5050 rule, which will actually teach you in class, but some some brokers will let you trade it. Personally, if you look at the stock, it's a penny stock. It's got no orders out there. You know, and I just said, you know what, you're dealing with the wild, wild West when it comes to this stock right here. So good thing. I would have made money on it, but we're losing one of our number one features that help us know how to trade. And that's the level three. Without that, we're trading blind. Another stock that's moving PSTV right here.  You could see the stock was not too long ago was at $16 one of the stocks that got destroyed. So this is one of the stocks I kind of like to trade. Because maybe now is the time it's going to make a little bit of a comeback. It does got some resistance levels a couple of days ago. So you can use it. It's got great orders there on the level three. So we'll keep an eye on that one. A little bit of a brand name stock, but it's been a great swing trade has been a mat. And AMD, you can see they're all doing very, very well. AMD is breaking, you know, great, great highs right here. But they're not really been the greatest day trading stocks, you know, you got to be careful with them. They moved to pretty damn volatile. You got to be a level three, level four type of trader to trade those stocks. You are see once again, with it, you know, if you looked at my, what I chatted earlier, what would I put it? Okay, I put it in a chat earlier. You nice stocks this morning spreads big JC Payne took a loss. I talked about that. What I put it in a chat. Oh, if you look in the chat, it says be careful of the stock right here.  You know what, Andrea, let the stock break a resistance. I don't have a problem paying like 220 230. But you know what, it's all over the place. Unless you're going to do nickels and dimes with this one, be very, very careful. I'd rather let it break out. But as of right now, it hasn't really done that. JC Payne, you could see good thing we sold that one. That one just literally just did a complete reversal, but it was a good swing trade. If you look at the long term, it's actually been making from 60 cents. I can't believe stock is still trading, or they didn't reverse stock split on it doesn't make any sense. Another stock that's moving really nice to that took a huge hit, starting to make a little bit of a comeback. Spread starting to get a little bit better right now is the FTCH. The stock is looking pretty nice. And I'm going to put the CGC, which we all know this is from yesterday. And it guess what, it's still breaking lower lows. So that was a really nice short right there on that one. Alright, anything I'm missing that I did not call out cyber traders? Anything else? Listen, wait the first five minutes of the open.  Let things pan out. You know, there's always new stocks that do come up when the market opens up.   So be very, very careful. You know what, I looked at that Neil JD, but it's not really going anywhere.  But it's kind of flattened pre markets in 730 this morning really has been sitting here. So kind of not really, you know, that's why I didn't put it on the list. Okay, and look at the tier sizes. One, one, one, seven, seven thousand one, one, 1300. I mean, definitely got a couple iceberg orders out there at specific prices, but not too not too excited about it. Remember, less risk, more reward. That's what it's all about. Okay, everyone.  Once you guys get yourself ready, get your cup of coffee, hit the restrooms. And because if you're in the trade, if you're not in the trade yet, we'll wait the next five minutes. All right, guys, good luck today. Happy trading. And we'll see you all back at 2 30 trade the afternoon. If you make your money early, take the money and run. Enjoy the weekend. Good luck, everyone. Happy trading.