Thanks everyone for coming we'll have now a workshop on formal verification of smart contracts and maybe before you jump into the topic so how many people have done any form of verification of contract so far maybe raise the hands so very few so I guess all the remaining ones will attract it by the last part that's supposed to be easy and hopefully by the end of this workshop everybody manages to you will have a hands-on exercise and everybody should be able to verify some formal properties on contracts so the people that will be doing the workshop we have a dimeter there is a student is joining change security now backgrounds in a form of verification and problem analysis then we have also until primitive so here's the developer of the very far that we'll be using today in the workshop also Hubert was sitting back there city of chain security and myself as well so who we are we are a chain security we are a spin-off from ETH Zurich ETH the University of the Foundation based in Zurich Switzerland and we focus on the blockchain security we have worked with many blockchain products so far we have done over 80 audits not only smart contract audits but also protocol audits platform audits as well as a couple of very visible EIPs I think many people are recognize the chain security name from you know some of those EIPs that we have reviewed in the past and so yeah we also have quite a few R&D security products with platforms such as Ethereum Foundation, Polkadot, Zilliqa and few other blockchains where we focus on building security tools you know tools for finding bugs as well as form of verification tools for these platforms all right so as far to do our work we have done quite a couple of systems so far so I have listed some of those some of them on this slide here and so this is the aim to achieve different goals we typically combine techniques from various different domains such as static analysis dynamic analysis we also use quite a lot of data-driven techniques for machine learning to you know to build these systems so some of you are familiar with the Securify this was the first system that we built back in 2017 it's a system for finding generic vulnerabilities in smart contracts and yeah so that's was basically addressing all these bugs that were popping up regularly every couple of weeks in 2017 in all these you know parity audits and many other contracts so this is what that system was addressing and so this system along with other system I think they made a difference in the sense that 2018 we actually saw much fewer hacks because of such generic like really simple boxing contracts so another system we have built is we have a fuzzing system that addresses the problem of ensuring functional correctness so we're going to talk a little bit more about what functional correctness actually means and we have a fuzzing system that's essentially generates transactions and tries to find violations of the specific security properties that we're trying to check for the smart contracts and the main system that we will be talking about today is the Verac system which is the first automated verifier for verifying smart contracts this we have a demo on Verac.ch we have set up a few other instances of this system that we will be using for the exercise later today and for people that are interested really in depth on how that system works what guarantees it provides so we also have a research paper which will appear at the IEEE symposium of security and privacy so that's one of the main security conferences one of the main academic security conferences so if you go on our web page www.chainseq.com and go to research you can download the PDF and read all the details about the verification technique that is being used in that system so before we actually do I will you know go into the hands-on exercises it's important also to mention why are we actually doing this and the main reason is that's I mean when I initially asked how many people have verified contracts I think there were about two three hands and the reason this is that you know formal verification used to be this very difficult time-consuming task where you have to be really an expert in formal verification have a PhD in logics and so on to prove that a contract is correct and if we are to make formal verification mainstream you know a lot of developers also adopting that approach then you have to be building assistance we have to be building systems that allow people without this background to write functional specifications and prove the contracts correct and that's exactly what this very very very far aims to do so it eliminates this necessary needs to know in-depth knowledge of formal verification and takes down this reduces also significantly the verification time because as we will see it's really not a very hard task to verify contracts with such systems so with such a system if you take something like a standard ERC-20 token which will look in-depth in the exercise you can literally do a full formal verification for all the main properties you would care about a token in a in a matter of couple of hours and be done with the verification effort. So I have listed here some of us some some of them that we have verified we have more on our main web page www.jensivirid.com or you can find some of some of these reports where we have done proper full verification of those. Alright so the workshop will continue as follows so we'll start with some very more high-level introduction to what functional correctness means and why is it challenging to formally verify properties with functional properties and what are different techniques that's different tools that are introduced in that space what how they different guarantees then so also we'll cover here of course the break system and then in the second half we'll switch to a hands-on exercise where Dimitar will walk you through how do we specify properties and verify them with a verify like verix and so we also have many other people from the chain security team back there so they will be assisting you while doing this exercise and then in the last part depending on time we'll try to get into some more detail about the actual verification methods and how this is being automated by the verix verifier. Alright so let's get started and functional correctness so what is functional correctness so usually when people think about security tools they're these kind of tools where you just paste the codes and then they show you a bunch of on the reasons are found so this is not what we're talking about here so we're not looking for generic vulnerabilities we're talking about functional correctness and what this means is that the problem of functional correctness has two parts so one is you have the smart contract that you want to prove that you want to make sure is correct and then the second piece of information that you need is the functional specification of a smart contract so what the functional specification is that this is the thing that this defines what is what is the intended correct behavior of that smart contract okay so to make this a little bit more concrete here on the left imagine you have a smart contract a typical year C20 contract so you have all these standard fields like balances, total supply, owner, a couple of functions that would allow users to transact for the contract and then the functional specification typically consists of requirements such as the sum of all balances equals the total supply okay so to give you this specification says that all the tokens are assigned to users somehow there are no missing tokens on a site to not assigned to any user another common example is that often tokens are invincible meaning that you can increase issue more tokens and often you want to ensure that only certain users can exercise this functionality and you want to make sure that if the total supply increases then that was triggered by a transaction issued by the owner of the contract okay and then typically you will have a huge list of those requirements that you will have to you will have to check that whatever the implementation these functions is it is correct with respect to these functional requirements okay so technically how does how do we actually check that the code is correct and they're roughly speaking two steps so the first step is well to essentially transform these English description of correct behavior into something that's to take them down and to specify them at the level of the source code okay so for instance if we take the first requirement that says that the sum of balances has to be equal to the total supply then this is written in the specification language that we'll be using later in the exercise of the very self specification language and this is how it will look in the actual specification language so fairly intuitive there's a seed some keyword point to the mapping that we're trying to sell and then we have a quality with the total supply okay so that's that number one it's inevitable you know we have to be able to transform any state what the property means and once we have formalized it then if we have a particular state of the smart contract then we can check the whether this property holds or not all right so for instance if we look at the state where we have two users having balance 50 each and we have total supply 100 and then the property holds that's that's what it says and here would be an example where the property doesn't hold because the sum of these two balances actually exceeds the total balance specified in the content okay it is clear so that's step number one define the property step number two is to actually check that this property holds for all possible states that your contract could reach okay now what does this again technically mean well once you deploy the smart contracts on the blockchain it is always initialized by the deployment script so it would end up in being some specific initial stage so that's what these days and you would have to make sure that the property goes there so for instance you deploy and then for that initial state the sum of balances will have to be called the total supply okay that's one then the next thing is that once deployed the users could send would send a transaction to the smart contracts and each transaction would modify the state of the smart contract so they can for example submit a min transaction with different you know different values as arguments and so on and let's get a little bit more precise what these arrows and boxes here represents so what these boxes represent is the actual state of the contract and the arrows are the transitions that are triggered by the transactions submitted by the users and how are how is how are these transitions defined this is defined by the implementation of the of the functions in the contract so for example if we have here the issue we start from a state where total supply is a hundred we have an owner user with address X10 and then we have two users with balances 50 tokens each and then main function is defined such that it would increment the total supply by the number of tokens we want to mint and then it will assign the new tokens to the to the owner to the owner of the contract so here if we have this mint 100 tokens issued by the user basically the total supply would be incremented as defined by the function and then the balance of the owner who has address 0x10 would be incremented from 50 to also 100 because that's how many additional tokens were issued okay so that's what these arrows here mean all right so here comes immediately the first in all immediate challenge when you talk about functional correctness is that even if we want to consider whether the property would hold after one single transaction after the first transaction sent to the contract that already gives you so many different transactions that you could that would be that would have to be accounted for that it becomes infeasible to brute force it's not possible to ignore these transactions and to actually check that in all these states the property would always hold and that's challenge number one and we cannot stop here because after the first transactions the user would send it second third and so on transaction and in fact there's not a predefined bounds on how many transactions this contract would process in this lifetime so we would have to consider unbounded number of transactions if we are to formally verify that this property would always hold okay so there are two fundamental challenges here so let's very quickly go over what are different techniques that could be used to address this problem of checking these formal properties and how they different types of guarantees and so I ordered a basic unreliability so starting from least reliable going towards more lab more reliable techniques well the bottom we have the manual review so always a human can look at the codes understand what it does and try to find violations so this is basically penetration testing we have the property and try to try to have the contracts and the disadvantage here fairly well known so it's a time-consuming problem even if you have especially if you have big contracts that would take a while for for the security expert to understand exactly how these things how how the functionality of the contract is then let's move over to more automated techniques so next level would be to do some form of automated testing and then primarily in general for software but also in the space of contracts to techniques for testing contracts so one is based on buzzing and the second major technique is tools based on symbolic execution so let's briefly see what this what these techniques would do to this problem of checking functional correctness and so starting for fun with fuzzing here's basically what's happening so fuzzing is a testing technique or a fuzzer would generate random transactions and then it will execute the transactions on the contract and by doing so it the fuzzer would observe different different states of the smart contract all right and by doing so we can for all the states that have been observed after processing these transactions that we generate we could check whether the property is violated or not if it happens that we reach a state where you get a violation then the fuzzer could also return that sequence of transaction that triggered the violation and the developer could see you know reproduce the buck and try to fix it there are many many fuzzer have been deployed that are available online that do exactly this this thing the challenge here typically is how to generate transactions in a smart way so you get very high coverage over at least a very high code coverage over the contract which is already pretty challenging and contracts which tend to be very stateful have complex preconditions and so on. So what fuzzing would not give you it would not give you this full guarantee that's why it's a testing technique because inevitably there will be some states that you would not not observe simply because the fuzzer did not generate that specific sequence of transaction that would transition the contract to that state so it's a testing technique essentially. Now symbolic execution that's something different symbolic technique that it is based on this symbolic execution technique it simply would not scale to reason about such depth of transaction so typically if you use a symbolic symbolic tool you would give it a timeout so it would run for maybe 30 minutes one hour and then you would stop and then it would reach certain depth so it is better at this kind of breadth exploration and but if the bugs are hidden deeper like after 5-10 transactions which could happen even in simple contracts like crowd sales where you have to transition to for example do some refund phase where you exercise and refund functionality but these typically tend to be somewhere lower that are harder to explore with symbolic tools. So I have listed here some of the open tools that are available that's to do this. Okay if this clears so far if there are any questions just raise your hand and then we can also go into a bit more detail. Alright so that's testing and then the highest level would be the conformal verification what this workshop would be about and this is really the point where you have a flip from testing to full verification meaning that you could actually prove that this property for whatever sequence of transactions you would make it would always hold no matter what. There is a major flip that happens at that point. Now so just visually what this means is that you will cover all possible states essentially and if you would check all of them and if you check more all of them you have this full guarantee. So that's what the variant system does and you will be using it soon and the input to that system is as we saw the smart contracts as well as the specification because we're dealing with functional correctness here and the main thing of that what the main thing that Verix does is it fully automates this process of fully automating the process of verifying in a sense that it's if it's successful it verifies the property it can guarantee that it is fully verified and if it fails to verify the property then it doesn't give a guarantee whether the property doesn't work or not. Okay so it could be that you have to help a little bit to actually verify the property or it could be that the property is violated and then you have to fix the contract. So we'll see some examples during the technical exercise later. All right so to give you a bit of so something that we actually spent quite some time is to ensure that Verix has a very intuitive and easy to use specification language because that typically is one of the bottleneck when we talk about functional correctness because again to use functional correctness in addition to the contract you have to write down what the contract is supposed to do and if this is very hard and tedious to specify you you know you would end up not really using the system. So I will give a few examples of specifications that we have seen to very frequently appear in real world smart contracts so this is something we just observed during audits and verifying contracts and so this is this is literally what the specifications are so you don't have to write some elaborate scripts or something very complicated to formally state a property. So common properties are things like access control where you want to ensure that certain functions can be involved by particular users for instance is saying that in always in the contract if there was a transaction to deposit then that was that transaction was made by the owner of the contract. Another common pattern that we observe is that very often it's not about who is sending a transaction but it won't in what state the contract is so for instance here we say that if the current time exceeds the refund time by a week then users are never no longer allowed to submit refund transactions. So yes state machine properties as well so again contracts are very stateful there is explicit state variables that define how the states how the contract can transition into different states so you have to make sure that these transitions are encode are implemented correctly in the contracts. We saw that example earlier as well so we have some over basically aggregations over mappings and arrays are also tend to be pretty common so that's we have added this explicit keywords in the language to allow users to to write these properties and another common pattern is that so typically if you have a project it's you don't implement the full product in a one contract but in several contracts and often there are certain invariants that so some sort of dependencies that are exist between the contracts and their properties that's captured these dependencies so you have to verify that they are implemented correctly in the contracts. Okay so again you will be writing some of these specifications so a bit more technically for people interested in logic so the specification language is actually based on something on a fragment of temporal logic which is very well studied specification language it goes, it takes decades of research in this so it has very well understood complexities and expressivity and so on. Alright so I would also like to depth on how how the verifier actually works but intuitively it combines two techniques one technique is it does use this symbolic execution technique which is very good at handling dealing with many different concrete values that you could submit in transactions and then to deal with the unbounded depth that users would submit it uses something called predicate abstraction that allows it to fully capture all the possible like this very large unbounded tree to capture it with some final representation so depending on time we may get into more details about that technique. Alright so that was the high-level intro and now we're going to transition into the actual exercise on how to use the exercise to specify this property so I'll hand over to Mitko who will introduce an example. Yes okay hi I'm Mitko yes and now we continue with a kind of small exercise how to use a verix. By the way if you have any questions at any time just raise your hand just speak and we can ask the questions the goal here is to make the exercise more interactive and not so kind of formal. Okay so so the first step in any kind of formal verification is to actually specify the properties informally. This means that you specify them in natural language whether it's English or some other language you just need to have some clarity over what this smart contract wants to do. And in this exercise we'll look at two main conflicts one is ERC-20 Tolkien and the other is kind of standard crowdsale of course simplified because we don't have too much time. Okay so first we'll go over specifying functional requirements informally. And when we go this is kind of fragmented of ERC-20 interface and for those who kind of are not so familiar with it the contract has let's say three main functions one is total supply how many tokens are in circulation. The other is balance of you can query how much tokens given address or account heads. And the actual main function here is the transfer function where the sender of the transaction can transfer some tokens from its own account to the recipient. So we have the address of this recipient's account and some amount of actor or any tokens sorry not actor but just tokens that want to transfer. And now whenever we are specifying behavior of contracts we do it over the contract and not over the interface. So here are the relevant parts of the actual contract right so the functions we have the balance the total supply and balance become fields of the contract right so these are not private fields. We have total supply as a mapping which says for every address or account how many tokens this address or account possesses right so this one is just an integer and this is a mapping from addresses to integers. And here we have some specification function transfer. Now when we're thinking about the contract or just specifying its correctness at least as a principle when I'm doing these things I never look into the implementation right so for me the contract is a black box and that's why I specifically omitted the body of the transfer function right. So now the goal is to just come up with a couple of properties hopefully full set of properties that specify the whole behavior of the contract. Okay good. So let's do this a little bit more interactive. First property is on me right so we already saw it actually and it says just informally in English total supply always equals the symbol power. So this kind of specifies an invariant meaning that it holds at all states of your contract something that you'd like to hold right and all we need to specify invariance about the transfer function right. So suppose you start the transaction with a given transfer function you have a specific recipient and specific amount and what would be the usual case of transfer? So I would say the amount of the sender needs to decrease the amount of the recipients needs to increase by the amount the balance of the recipient needs to increase amount and the total supply is not allowed to change. The total supply is not allowed to change yes you're right yes so this is very good requirement we can allow right a little bit more so just to repeat right you decrease the sender's account by the given amount you increase the recipients account by the given amount and total supply should remain the same right but one thing for example that we will meet it is that so we said the total supply should be the same but this transfer could have transfer tokens from another account right so we didn't specify this so what we did is a partial specification right so in addition to that we need to specify that all other accounts remain unchanged it's not just the total supply and as a consequence the total supply will also remain unchanged right okay so we also do this in the case the sender's account has sufficient funds right sufficient amount of tokens if it doesn't have the function should not do anything right so the first case a little bit more elaborately right is if the message sender is not equal to the recipient right otherwise you don't have anything to do and there is sufficient amount of tokens in the balance of the message sender then the message sender's account or balance should be decreased amount the balance of the recipient should be increased by the given amount and all remaining balances should be made a change right this is kind of a fairly straightforward informal specification so what will be the remaining balance so we have one more case to do here any clue number of balances should be the same as number of addresses number of balances I mean the yes yes you're correct number of balances should be the same as number of addresses this is kind of implicitly assumed so if we go back a little this is kind of implicitly assumed we have this mapping it is kind of you continue it containing account for everybody every possible address in the world it's very large amount all the possible addresses it's really kind of the ethereum kind of language and security language takes care of this but this is a correct thing yes so what we do is we consider the alternative case right so we have this if here alternative is to logically negate the condition which means that if the message sender is the recipient or the balances are not sufficient right all balances should remain unmodified right yes I'm not taking into account our flow at this point yes you're absolutely right so when you're doing specification is very easy to miss something well also the same way as as you're probably something for example here it could happen that these conditions here are satisfied when overhaul for happens because we have more than a day here we didn't go with addition and subtraction everything works fine even if you overhaul something and the problem is when you overhaul something the actual amount is not the amount is that in general you don't take into account or just in this example I don't take it into account so what you can do with Varex is depending on your property you can specify in such a way that it would automatically fail to verify if all walls happen right but what we currently do with Varex is that we don't explicitly check for overflows right you need to write your property in such a way that it fails even if it is okay and the other thing is you can think of the specification at the informal level as referring to actual integers where there is no overhaul right this is kind of just the informal part but when you go to actual formal verification you cannot think of it this way right okay so this is informal requirements for ESC when okay now let's go to something slightly more elaborate so we have a crowd sale and the crowd sale has a couple fields so a crowd sale contract the amount of either which is raised the goal factor which you want to raise and the closing time of the crowd sale and the behavior of the contract is that whenever somebody sends money through the invest function right this is a payable function the crowd sale contract will deposit this money into the escrow right and when somebody walks close and it's about time to get close right after the close time has passed then depending on this we have two options either the goal was raised in which case the beneficiary of the crowd sale can withdraw the money from the escrow or the goal was not raised in which case the investors can claim the refund for their actor which will be set and this logic should be realized in the escrow so here what you do have is mapping your deposits how many how much actor each other is deposited in the escrow and the beneficiary who in case of success will receive all the money right so let's let's try to specify this again inform right so again let's do the first one so the goal and close time always remain same right so so this might look like a stupid informal requirement but in insularity these things can change right this keeps your contract these are stored in the storage potentially they can change so because of this we need to be explicit about which things need to remain constant or which things can change right so this is a requirement that is all often missed and people can yeah okay other suggestions right so so just to implement kind of the logic that we informally describe now in informal like no need to be very precise this close on the work if you pass sorry close only will belong the work if you pass close time close will only work if you pass the close time yes so what does this mean close will only work if you pass the close time sorry now it's larger than close time well like if now it's less than close time called close must be very successful must be done successful yes yes so you can specify this this is one option let me see what's the next property I specify here is because yes but maybe maybe it's something along the lines of close so what does he say soon no it's it's something else right so so here just for the sake of the workshop I have the properties fixed so you are welcome to say properties I will not have them to the slides here we just work with some things as the properties and property be yes a similar investor deposits equals the actor in escrow unless success right so this means that you cannot withdraw or change money from escrow is success right okay so let's see some something more escrow never allows both withdrawing and claim the reference right so this was one of the requirements we specify and more more yes investors cannot claim refunds after crowdsale goal is reached and maybe you can figure out what would be the complement of this not compliment the complimentary or the extra property needed to counter part this this behavior yes beneficiary can withdraw after crowdsale beneficiary can only withdraw after crowdsale goal is reached yes beneficiary can only withdraw unless callable is rich you can say something in many ways so yes but it's the same so beneficiary cannot withdraw before crowdsale goal is rich right so we have these five properties now this is most likely in complete specification of the behavior of the health so providing a full complete specification is kind of difficult exercise and whenever you are verifying your contracts you don't need to do it right but this means that you should always keep in mind the possibility that you need something right okay so now we have a bunch of properties and what we can do is we can just attempt to formalize them and specify them in the verdict specification language and I okay any questions is as you're going through the requirements is you saw that if you go back to the specific interface for the contract the crowd sale there are three states open yes success and refund yes but there's there another state where the you've reached the goal it's closed but the beneficiary hasn't gotten around to claiming the thing so it's kind of pending is my question is with regard to the interaction between this code and the specification you go back and forth and change the this code based on your understanding of the specification so if you're to develop the contract together with the specification yes this is how it's going to do that right you will do back and forth like you write your requirements if you see that you miss something you change the code and maybe on the other hand you did something in the specification which is wrong and the code replacing correctly to change the specification it's so this process you can miss out because it seems like here there would be some kind of limbo state where there will be a mistake yes absolutely there will be a limbo state once the cross time has reached and is closed by the who is not called right the as problem still be in an open state and you cannot do anything basically you this is because maybe the beneficiary never gets around maybe they got vaporized and that's you know so it remains a little state forever so okay so they need to make a requirement that you can escape the state right you make a next requirement as I said specification with the PC so there is something else I need to tell what you said you can escape the limbo state this is called the liveness property and flags actually cannot verify liveness properties they are different techniques and what we focus on properties of these kinds which are called safety properties yes but I'm not getting too much detail about this yes this kind of a reverse shouldn't you have the formal requirement first before depends on your style how they how develop the code right so some people prefer to write the code so they understand the problem you might better and then develop the specification some people try to develop the specification before they understand it also if you're providing an audit service you're not writing the code you're you're hired to yes this is what people in chains I do yes they they don't touch the code or they give suggestions about the code to change but in general yes we do write specifications sometimes based on the code sometimes based on the requirements given by the clients yes what about the investment function in this yes after the goal is reached whether you can invest after the goal is reached it should not be possible you should not be possible to invest once the crowd sale ended in some way yes absolutely I said the specification is incomplete right right so ideally you'll get a complete specification but this is an open-ended process requires something okay so this one the whole point of this is to emphasize that before you start with formal specification it's good to have informal one right just to have a clue what you want good so okay let's move on verify things with Variks we'll try to formalize these properties in the specification language that Variks supports and see whether they verify or not okay so how things get into the specification language and Variks is based on something called linear temporal logic so this one sounds scary but it's something very natural so let me try to just give a brief explanation so maybe most of you are familiar with classical logic this is our everyday logic that we use and you can express formalized properties for example the age of values was the age of what is even right so classical logic defines the relations between individuals in this case the relation is that the sum of the ages is even right and how would you write this formally in classical logic you say there exists some integer such that age of values with the age of both is twice this integer right so kind of to say the things are even right this is classical logic and temporal logic adds another dimension to this which is time right so things are not just statically laid out in a perfect ideal but we also have progress and temporal logic also is to define relations across states so you have usually initial state in time point zero that you have point one you have another state and so on and so on and so now you can define a relation between those states and here we just as an example such a relation says it's always the case that the age of values is even right so we've just changed the property very slightly by adding the always kind of temporal operator to express this this relation which is across time not just within the single state right so you see that this this this relation does not hold in the real world right it's cannot be always the case the ages are even and somebody the same increments age one guy increments age the same will be comfortable right so this is an example of property that does not hold because it's not always the case sorry unless they're twins unless they're twins or it's born on the same you're obviously yes I forgot so yes so just to say what you're specifying with the temporal logic what you do have is this model kind of you specify properties of traces or formally and each trace is a sequence of states right the index of the sequence gives you kind of discrete time so time progresses from zero to infinity going the increments of one right so for example this could be the zero state or some people like to come from one state and this is the second state this is the third state so this is kind of what you're specifying in temporal logic and each state we can kind of divide the worlds or two parts that the constant inside the states and the variables inside the state and as an example Alice is a person is a constant which means that it this object does not change across time Alice remains Alice in all time points right the same goes with numbers possible ages and 27, 28 what not right so these things are constant they never change the cross time and the other part of the state are variables in this example is age so variables can change across time this this is briefly kind of what the statement contains, contains constants and values right and now when we write a formula right we want to interpret some statement about time it's good to say what the mental model is and how you evaluate those things so here is a different example we have temperature right so we have states and our state contains constant is some temperature and the variable is the temperature in this state right so time could be days in this case so we did not specify it in what units the time is measured it's on the screen unit I think we want to see is this property here it says eventually always the temperature is at least 11 degrees right so we have some property and in order to see whether this is true for this trace so this is the trace right we need to see whether this is true what we do we start evaluating the truth of the sub formulas for the parts of this sentence across the states and for example the kind of the innermost part is temperature is at least 11 degrees right so now we just see at which states this statement is true right within each statement we are kind of almost like a classical logic but not real right and here we can see the temperature is 11 degrees in the first state in the third state and the last two states here so time can continue for all right assume the temperature remains at least 11 degrees forward right so this is where this part of our statement holds true now in order to see in which states the always at least 11 degrees holds true we need to look at the sub formula and see whether it always holds right so always means that maybe better term for this is has for right so we can ask the question is it always the case the temperature is at least 11 degrees in the initial state and it's not the true because in the subsequent state the temperature is 10 degrees it's no longer at least 11 right so it's not always the case that the temperature is the place 11 degrees in the initial state it's also not always the case that it's in all these states until the temperature stabilizes or let's say goes below 11 degrees forever so from this point onwards this part of the formula will devaluate to true right so it's always the case the temperature is 11 degrees and now the final kind of temporal operator you're looking at here is eventually the case that always the temperature is 11 degrees and eventually is true in a given state if there is a future state where the sub sentence that you already is right so in which states is the full sentence true that's how it is guess everything everything yes because no matter which state I evaluate this this formula here there is always a future state where it's always the case that the temperature is at least 11 degrees and this yellow light in which states it's all these I guess I don't understand the meaning of that future state because how do you know that's true or not because there's the heat death of the universe where the temperature will not be so so so this is just an example it's an example when there is no we don't know if there's gonna be a heat death or not so okay okay you're absolutely correct so for this sentence as humans we cannot evaluate but avoiding blindness properties verification problem is yes more questions okay good so let's do a small quiz just to see how this temporal logic works right and here this is very unfortunate because this should be a circle so we have two squares which is very unfortunate it's a printable character yes yes these phones don't have it anyway it's the ball square right so we use the small square to say always how do you say the diamond to say eventually and the ball square to use next something is doing the next step so what does this sentence say right you have two formulas or two predicates P and Q and this thing says he implies that eventually Q right this is what it says so how do you interpret this informally what do you understand from this okay let me help you if there's P there will eventually Q will happen yes if there's P yes so so yes I put this example just to emphasize something when we are evaluating a formula we're evaluating it always in the initial state right so there is a slight kind of something in subscale written time we're always evaluating a formula in the initial state so you're almost yes right we evaluate this in the initial state is if initially P is true then in some future moments or the current moment actually eventually it's not straight but it's all the current moment Q holds and what you said you can formalize with it's always the case if it holds eventually Q right so no matter whether it's initial state or initial state for every state in these holds okay so what about this one always eventually P you just get some alternative description of this formula yes it's impossible for P never happen yes you can play with the Morgan's laws yes yes this is alternative description is valid another one yes exactly yes so you can interpret this because we have kind of time running clean theory you say P is too effectively often it's always the case of eventually P holds but if we eventually dissolve hold in some future state it also must eventually hold so this will repeat infinitely often right and what about this one if we swap eventually always P holds yes okay I just want to talk about some more I want to describe here absolutely as if you just read some facial phrase can spell out well what it's written it is what it is this basically says that eventually P stabilizes kind of from certain moments onwards P will always hold this is always this right well we have three more so so we got into this one so what does it say yes from any state that P is true Q is true that state and every state after in every state after and why is this the case this is true you're correct yes because the always you on the right this is this is the ball square which is next but it's true actually what you said right so if you interpret this next as next right it's always the case right if people then in the next case never people never be true why people never be true because then the next state would be Q and they are not mutually exclusive I'm not usually exclusive they're not so they're just he is always followed by yes he's always followed by this is it right and all you have what you said right is if people's afterwards onwards until infinity if you would hope good so these are the more simple ones one of us I don't know why put so many but okay so this one is more complex it says it's always the case there is some constant and such that in this case the clock equals them and in the next case clock equals yes yes the clock always increments by one this is this is all these properties I just wanted so this is kind of full temporal logic right you can write many complex formulas and statements in full temporal logic code always clicks or peaks by one increment it's correct because the clock actually the time yes the clock it depends on computer clock if it's digital clock or some unique timestamp or whatever it is depends on the yeah yeah doesn't wrap around sorry okay so for for for the standard clock it doesn't work okay yes okay good so now how all these applies to smart companies right so what we do here we need to fix what time needs first first and foremost and what we do is we do the following we have world states and the world states are the states of the whole blockchain in between right so whenever you're thinking some blockchain you always around the thing inside of such and our state will be the world state of the blockchain and time increment means the execution of a single transaction right this is what we do and we don't support the full temporal logic it's about just a fragment of it which is called canonical safety fragment but they're not gone in details and roughly it looks like this you always your formulas of this form always P where P some formula of the following shape so you have logical conjunctions P and Q you have this junction P or you have implication P implies you have this very interesting operator which is temporal operator once P which means that once in the past people is holding this is the time reversal of the eventually operator so we had eventually meaning in future moment P will hold this means that in the past he was holding or the current state yes at least once or at least once exactly so it's not exactly once at least once so in some past state P was holding this is what we do and finally whenever you have some expression you can refer to the previous value of this expression so this is similar to the next operator so in the previous state the value of this expression was something right so here we were refer to the previous value of the expression these are the basic things by the way what happens in the initial state where there is no previous state what do you think so when there was no initial state just for simplicity we take the priors with the current like in the initial state just remember this I mean sometimes it's no yes yes okay and now we have some ethereal specific things because we are after all doing things on ethereal so one thing is we support sum of mappings right so in balances is a mapping inside the token contract we can refer to the sum of all these things function returns the the name of the function which is called in this transaction the top-level function right so we have nested calls we kind of abstract these nested calls away we we can refer only to the top-level transaction the function in the top-level transaction we can refer to function names so this is the syntax for referring to a function name and we can also refer to arguments of functions so syntax is a little bit improvised we're going to improve it in the future so this is the zero arguments of the claim refer function and here what you do is you do canonical name of the function so this is the name of the counter table function and here if you put the signature of the function with the addresses right this is what happens yes okay you just shout okay you shout so so we don't support specification of loop invariance so all we do is basically specify let's call it transaction invariance something that holds across those options what if we have no TV loose in the country so in some cases we can rewrite them rewrite them without loops but if you have no table loops we unfortunately don't support it yes yes I have forgotten yes there is also negation so yes I forgot the negation yes so we got this but you said earlier that you know you evaluated formula always in the initial state in classical temporal yes so what's this is the semantics different now and we know it's the same it just that we support formulas of the shape always be right not that's for the for the operators once and previous if we're always evaluating in the initial state so you evaluate the top level of the formula in the initial state right but it could happen that when you say always this means that the inner part of the formula needs to be evaluated in all states this is the semantics of the always operator so from formula to sub formula you change the point at which you evaluate right depending on the semantics of the temporal operators which is the point at which you evaluate the formula right so always changes the point at which you evaluate you evaluate in all points from the current point on this that's the idea so you evaluate formulas always in all states okay good so now let's move on to small quick question on that box on the left you have once a previous there's no next there is no next we don't support it yes we're somewhat limited but many things that you can express with next actually you can express in this way just you need to massage your formula not everything that's okay but you do you have negation there that was just I forgot yes yes we don't negation yes we require always to be the top level right so never again yes you cannot negate yeah never again yes this is always he is given by this index plus negation you always have to have always you always have to pay always sorry do you write it down yes we were writing down in the formula so it's explicit yes this is basically what you can specify is contract invariance contract invariance exactly you can say this way yes but you also can refer to the past that's that's the kind of cool thing so I'm just curious why not next I mean is there I'm not familiar with the verification technology so is there a technical reason why next is more difficult than previous so for verification it's slightly more difficult yes you need to do some gymnastics okay and when you are eventually becomes more difficult way more difficult because once you always look finite number of steps in the past because in the past time is limited is bound but in the future it's unbounded eventually things become very very infinite that's good okay so maybe you just go quit your exercises so now it's time to formalize what we need and just to love balance our very fire we have two servers in which you can run by X there is nothing using interface let's say this part of the room uses by X1 and the other part of the room uses by X2 as can we do it like this because the service are powerful but the vacations okay sorry just general is very some online too long here is it downloadable the more it It's online too. We hope to outsource it in the future. Okay, so there are two servers, left part of the room, right part of the room. And for Varex intakes, you can click this link and check out the links. Yes. Okay, so if you open the links, you'll see this kind of interface to Varex. On the left, what you have is a list of contracts plus specifications. So we preloaded Varex with a couple of contracts and currently we focus on the ERC20 and ERC, sorry, and CrownServe, right? So we have two contracts which we focus on and the entries, the surface with solution are the solutions to those exercises, right? We have three extra exercises which you can do, but maybe there will be no time for this today. They have no solutions, so you need to kind of give it a little bit more on that, about it. Okay, good. Yes. Why not to be on our questions all the time? Well, I'm wondering how do you do these state predicates? Is all of the state predicates success? Can I define one as a user, for instance? As a user? Okay, let me, maybe, maybe, yes. No, no, no, no solution. Let me use. So you give a list of formulas, later we'll talk about the remaining formulas, but what's important is the first formula. So the first formula gives you your problem. And it has this formula, O is, and then some formula. So whenever you're specifying something, and then you have a table which gives you more details, the syntax, and for example, you can refer to contract fields using contract block fields, right? So you can refer to the contract state this way. I forgot some of the syntax details, right? Also, you can refer to message sender, you can refer to the current time, the time in this world state. I forgot the block. Yes. So, let's see. So I guess I don't see an end on the state predicate. State predicate's very meaningful. In some, are these in the state? I, I guess it's like, it will try, like, actually, if it's double the quality of the state, right? Yeah, I guess, I guess, yeah. Ah, yeah. There's a lot, there's a lot. There's a lot, there's a lot.   Yeah, you have an example with like success or refund, that the state predicate's on the success state, or even on the state, or something like that. Ah, okay, okay. Yes. Okay, let me just give you a short demonstration about the first property. I thought of why OEC equals the same imbalances. So. Okay, so, yes, Petter will write the first property, right? This one is simple one. Say always. Talking under the same imbalances. So it's the case that the same imbalances equals the total supply. Yes, this is it. And if it goes scroll down, there's a verify. What's a verify? You see on verify. And it's a point in front. Verification takes some time. You see that the property, the first one is cute, which means it's a pending state. It's not know what a verify is or not. And the other problem is failed verify. So you need to verification takes some time. So you cannot, it's not how to say a tool where you get immediate feedback, you just verification takes some time. I don't know about your approach to that. Why does it take so long? It takes so long because we analyzed the vital level. And the very small problem you heard about yesterday, does it very small. Very small is a tool from Microsoft. It verifies it on the last time symptoms, which is kind of the high level semantics. And then it can be faster. Does that mean some op codes are supportive, or does that mean somewhere before, at the moment it was in your paper I was reading it, but that's the reason why there was... Delegate code, for example, is unsupported. There's some op codes that are unsupported. In some op codes it's unsupported. When you have delegated code, it's very easy to break any property. What would you say?


The Ministry of Equity, Social Justice, local government and empowerment through the Department of Human Services has assisted with the construction of a house for an elderly Dennery resident, Gilton Joseph, contractor Collins Lynch, volunteered to build the structure. His company, Triple L, provided the materials and labour. Projects like that, we, more people need to get involved with because just going around the community have so many people who need that help and I understand what is happening and I'm going to do my best once I can, I will. Like I said, in the past I probably do maybe 15 or 20 of these projects in the last 10 years around the valley, Dennery already. I'm hoping I can get the strength and help from God to continue to do this. On behalf of the Ministry of Equity, particularly the Division of Human Services, elder care units, we would like to say thank you for doing this beautiful project for Mr. Gilton. We're very grateful. We're happy, he's comfortable and we're actually saving one older person to be comfortable for the rest of the years. So we appreciate you. We appreciate your guys, your company and we thank you very much. I would like to say thank you to Mr. Lynch for the great work he did because Mr. Joseph was living in a deplorable condition and he came on board, he assisted us and we are thankful for what he did.


Good morning everybody. So, just gonna talk about what we're gonna get into today. I'm gonna do a brief introduction about myself, kind of my background, what my interest is, kind of my passion about continuous integration and continuous delivery deployment. I want to mention the session right after me goes into a lot more detail that Kruna was saying right there. It's gonna go into more detail on our continuous environment setup and give a little bit more of the kind of details on how it's set up and how it works. I kind of wanted to... I usually do this presentation just focused on what we're doing, but I kind of wanted to give a little bit more info on the landscape, so I kind of wanted to talk about the evolution of what the platform is today, how it's evolved, where it started, and, you know, understanding that, and then the evolution of how DevOps and how its landscape has changed considerably, I would say, in the last five to ten years. And I'm gonna talk about some of the DevOps infrastructure components and tools that we're using and how this relates and how to integrate your GitHub or your project with our DevOps infrastructure. And then I'm gonna do a brief demo of the pipeline. I did, unfortunately, record. I did not want to tempt the demo gods or the conference Wi-Fi or network. So I can show some live stuff, but I recorded most everything. I'm just gonna talk through that demo. And then I'm gonna talk about kind of what the future of DevOps infrastructure and CI CD, kind of where it's headed, some of the new innovations that are happening in the space, mostly around OpenShift and Kubernetes. So Spoiler Alert will be talking a lot about OpenShift and Kubernetes. So my name is Riley Vigny. I'm a senior principal software engineer at Red Hat. I am in the system engineering organization and I'm on a continuous productization team. So what that means is that, you know, we're focused on how we can release our products with more efficiently, you know, quicker to the release and also with less bugs. And how do we enable that process? So we're working on a lot of things internally, like a service to help enable that. So users don't have to figure that, or developers and QE folks don't have to figure that out themselves. And, you know, at the end of the day, my passion really is continuous integration, continuous delivery in the overall DevOps umbrella that encompasses that. Again, don't forget to go to Kronos Talk after mine, too. Just wanted to mention that again. So the evolution of the platform landscape. So, you know, everything kind of started. The platform was, you know, you install your OS on a bare metal machine way back when, right? We all had, we all did that. And then that kind of went to the virtualization stack. So there's, with all these different pieces, right, we just had machines and there was kind of no consistency between them.  But it's not very repeatable or consistent. Then, you know, obviously you could use configuration management to do some of those things that helped out there considerably. And then we go into the cloud where now you could get your VMs and all your components via any of these clouds. And so there's ones that I've left off, but these are some of the examples of what exists today. To me, really, the evolution of where we've come to is Kubernetes and OpenShift in particular, which is kind of red hat spin on Kubernetes or their distribution of Kubernetes cluster and install. You know, kind of the history here of how it's grown and how fast it's grown is the first DockerCon was in 2014. The first KubeCon was actually two years ago. There was a thousand people there. The KubeCon this year that I went to in Seattle, there was eight times as many people there. So think about that for a second of where it started and also the original projects that were part of the Kubernetes umbrella were these three. Kubernetes, obviously, Prometheus and Fluentd. Now, if you look at the landscape of what is offered via Kubernetes and the projects that have grown out of them, whether they're in the sandbox or incubation or graduated stages, over 30 projects. And that's really because people identified that this is really the new platform. This thing that is running on top of bare metal or VMs is really where you can have consistency in rolling out your applications and any of the systems that you want to run on top of that. That means, too, right, it doesn't really matter if you have a cluster on-prem or you have it in a cloud. That experience is pretty much the same across the board, which is probably different than what previous platforms offered you. So I think that's really important and that's what's really kind of also evolved the DevOps landscape of how we set things up and on a platform. So like I mentioned before, there is configuration management. There's a lot of these tools that have evolved. Ansible, CF Engine, kind of that's what's current, right? I mean, that's what people kind of use today or have been using. Kind of the new stuff around configuration management is maybe APBs, which is the Ansible Playbook bundles. And then monitoring on some of these systems, we used to use Nagios and Xabix. And now in the cluster itself, we're using Prometheus to do some of this monitoring. So just as kind of the platform has converged into, now we have Kubernetes and OpenShift, which is an application, it is a platform to run any of our applications that we want, whether it's databases or front-ends, back-ends for it. Some of these tools have also come together. Obviously, I didn't put a current and new on the CI-CD tools because I think all of these are still relevant and still evolving. Some of these are services, and some of these are just straight tools. Obviously, CircleCI is a service, just like TravisCI is a service. Zool, Jenkins, and are really more along of tools that you can implement yourself or get maybe some off-the-shelf implementations of them. Like in the case of CloudBees is the main contributors and owners of Jenkins itself. Zool is definitely open source and has been very accepted in the OpenStack community and now is kind of expanding out to other facets. So a lot of these things are converging together on the platform itself. A lot of companies are making moves now, not just to have a separate CI system that runs, but really more around how do we actually implement this or integrate this into the platform itself, and that's really what I'm going to get to when I show my demo and we talk about this stuff. The one thing I wanted to also point out about Jenkins, Jenkins Classic is not cloud-native. It's not Kubernetes-ready. It's really just a job application that runs. But then it got containerized, which is cool. It's containerized. That's great. But it's still not really cloud-native aware. You can't scale it. You can't really... It's not ephemeral in the sense of you could spin that up and spin it down to do a task, and it's gone in a pod on OpenShift or Kubernetes. And then it got a little bit more, can we run this in a pod and a little more? Now we're actually... What Jenkins and CloudBees are doing, part of this evolution, is to make Jenkins more cloud-native and more available, and there's this thing called Jenkins FileRunner. So now you could actually spin up a headless Jenkins that's just there for the orchestration to execute Jenkins pipelines without having to have that persistent and sitting around. You don't have to have storage to back it or do any of that. You can actually collect the logs off of it, any of the artifacts, and push them to another location. So that's kind of where CloudBees recognize that Jenkins itself is not really kind of meeting the muster of running on OpenShift or Kubernetes as a platform. So how do they actually change that? Some of you may have heard of Jenkins X, which is actually their complete, I would say OpenShift or Kubernetes cluster solution there that runs on a cluster. And so the other, I think the other interesting thing too, I went to Jenkins World this past year and for the past, I've been there probably the past four or five years, the conference was always called Jenkins World. This is the first year that now it's called Jenkins World and DevOps World. So they're shifting away from Jenkins being their flagship product because they identify that DevOps is the space that they want to get to and how do they actually enhance that with their products. So it's not just going to be Jenkins and how do they actually run that on top of OpenShift or in their case probably Kubernetes. So I'm going to talk about some of the infrastructure components and tools that we use. So obviously on OpenShift we have this thing called S2I Templates which is just a configuration, a YAML configuration of a build config to put on your Kubernetes cluster. When I say Kubernetes in OpenShift, interchangeable, let's just assume that. And Dockerfiles that we want to load. In the case of Jenkins, we're using Jenkins for this demo and that means you have to use Jenkins but we have shared libraries and pipelines that we also roll out so it's an optional piece and then we also have this thing called Hooks where after we actually run the setup here, we then can do some any post-processing. So I'm going to show you today in the demo before I get to that is an OpenShift instance locally run on Minishift but the same stuff that I'm showing you could also easily have an OpenShift endpoint that we just apply that to and can roll out these S2I Templates, our containers, any Jenkins pipelines and run any post-hooks that we want to after the cluster has been set up. The other thing that our team has worked on is this thing called Contra-HDSL, all upstream projects by the way and I'll have links at the end of the presentation for that. It's really a simple YAML DSL that is a front-end for Jenkins libraries and pipelines. So a lot of people don't want to have to know Jenkins or no pipelines or what that entails. This allows you very easily with some helper containers that we build in OpenShift and then we deploy at the time when we run a pipeline. One is called our Linchpin Executor which is used in their helper containers and that's used to provision resources in any cloud. So even if you needed a bare-metal machine or a VM in AWS or GCE or OpenStack you could use this mechanism to do that and then we have an Ansible Executor Container, another helper container that also helps configure that resource once it's been provisioned, executes tests, and then collects logs and artifacts. So a very simple workflow. The pipeline code for that is a little bit more annoying to have to maintain our libraries so we've kind of handled that for you and used these helper containers to help administer that. And now this is kind of, I'm going to lay out kind of how all our stuff comes together here. So as you can see, I blocked out this future stuff because I'm going to have that bring this back up on the future slide of where kind of we're headed with this but I wanted to at least have the whole diagram up here. So whether it's MiniShift at the bottom here or OpenShift, whether it's a stage or product and production environment or your local MiniShift, you have this one playbook that will set up a cluster for you. It will, we have a, our Contra, NV, Infra, the pink area here that has the future stuff blocked out. Has our helper containers, any of our metrics containers like DB and Grafana and all the Jenkins infrastructure already ready to deploy and roll out. If you have any pipelines, we have some sample pipelines in this HDSL code here on the left that can be deployed if you so choose. It doesn't have to be. Same for the infrastructure. If you did not want any of these pieces, you can leave that out. And then we come to this yellow stuff on the right side. This is you guys. This is your project that has been designed to actually build and deploy on the MiniShift or OpenShift infrastructure. This allows you to do that. So this kind of lays all that out. A crew no product is going to go into a little more detail on some of that, but that kind of shows everything that we're working with across the board. And when I show the demo, you'll get to see some of that firsthand. So everything comes down to kind of this. You could do, it's all Ansible based. So you could do the parameters one by one, or you could just generate this kind of file that I have here, this contra-NV setup, which is just a bunch of parameters which I'll walk through as well. The S2Y templates that are in this project, the Dockerfiles and the Jacobs libraries and pipelines, like I mentioned before. And this is basically the structure of the sample project that I did for the conference, which will be available afterwards and the references on the slides. So this is that file. Some easy parameters. Cleaning up things. We don't want to run pre-rexes really for virtualization, nested virtualization, which in this case we don't care about. I'm going to set up my containers. I'm also going to set up pipelines. I don't want to set up this sample project. And I don't want to modify any of the security context. I am setting up MiniShift here and my profile's name is MiniShift. It can be whatever you want to call it, but for this example and for the demo, that's what I chose. And this shows the MiniShift version and the OpenShift version that you're going to use with it and some basic username and password that would be set up. And then the bottom of this file is some of the other stuff. So Kruno actually added this feature of whitelist and blacklist. In this case for this demo, I really don't want my helper container, so I'm going to actually leave those off of the installation. What that means is that the diagram I showed you where the infra setup had those helper containers listed there, it will then identify that these two would be ones that we do not deploy or build in the environment at all. And then here's the name of my OpenShift namespace and the project repo that I'm going to be using. You can go to that URL and all the stuff that I'm showing you here today is available there. And then just some information about the memory and CPUs that I want to provide for my MiniShift instance. There are more things down below, but less important, more around the influx DB and Grafana setup, and you can look through that as you wish. All right, so we're ready to do a demo. Really, this is the command that I did to kick off the demo, so I just wanted to show that there, and it's in the slides, but let me bring the video over. So I'm going to talk through the video. So I just did some pre-clean-up I did before I ran the demo from scratch. So I cloned the Contra-NV setup repo, and then I also cloned my project repo, which in this case is the DevConf demo. That's really all you need to get started with this. And at this point now I'm ready actually to commit to kick off that command line that I just showed you on that demo slide. Actually, sorry. Just so you can see the file that I just showed you in the demo. I'll also make this video available after the conference, too. I'm just going to skip through some of this. Sorry about that. So here's the command line that we're kicking off. I just have to put in my password, but that was the same command line. Actually, if I just want to back it up just a bit. So all I did was I provided my user on my system, and then I pointed to that setup file, and then I provided the sudo, so it asked me for my password and my SSH password, and then we can proceed. So it's going to go through, in my case, and up the previous cluster that I had set up there. So we'll do that, too, because I had that run clean up option. And at this point it's going to go get the mini shift binary and then start actually creating the cluster. So it's going to deploy a mini shift, basically a VM, and then once the VM is up and running, then it actually deploys the version of OpenShift that I want. In this case it's 311. It also pulls down the OC binary, so you can do OC commands as well. So now we're at the point where we already, the mini shift cluster is set up, and now from my project I'm deploying this Fedora image and that has come from a Docker file, the S2Y template. I'm just going to get the IP here of the actual VM that's running my OpenShift environment. And at this point I've kicked off and I'm waiting for this Fedora container to build so that it's available, but even before that we can log into the mini shift instance and then have a full up and running OpenShift cluster at that point. We can go to our devconf namespace. There's nothing deployed here yet, but you can see when we go to builds here that we've already built, or we're in the process of building the Fedora container that's actually from my project. It's not in the infrastructure pieces. So at this point, after it does that first project, Fedora container, it's now going to go to the helper containers, which is the Jenkins master, slave, and as well as the Grafana and InfluxDB containers as well. We also have a container tools, which has Builda and Podman also, part of our helper containers. It also gets rolled out as well. Let's speed this up. So I don't want to fast forward too much, but so now we're in the process of just finishing up building of these containers and you can see we just had Fedora before. Now all these are either complete or in a running state that they've been deployed to the MyMiniShift instance. And until those, since the Grafana, Jenkins, and Influx have deployment configs, after they're built they get deployed out to the OpenShift instance. And I can show you that too. You can also do, since you have OC available, you can also, besides the UI, you can do this on the command line and see the same containers or see the complete setup of everything that's on that cluster at this point. This gives you a full view of that. Sorry about the video choppiness. So now at this point, everything has gotten built and now we are deploying our Influx DB, Grafana, and Jenkins as well. So Jenkins is the last one to come up. Grafana is now deployed, Influx DB, and Jenkins is in the process of the pod coming up, I believe. But we can go to the Grafana UI at this point. It's up and running. And this is all locally on my machine. It could be we could take this whole thing and deploy this and skip the mini-shift part and deploy this to an OpenShift cluster. That's perfectly feasible as well. So Jenkins is still coming up. Now, all the playbooks have finished running that full system. And it takes about, if you're deploying mini-shift, it could take from anywhere from 15 minutes to 20 minutes, something like that. And then once this is deployed, then we'll have a Jenkins instance that we can go to and see the end part of this, now that this is all set up and that's great, now how do we utilize that? So we have a pipeline that we seeded. We have a seed job that picks up that pipeline file. And then it runs basically a stress test to get stress to CPU and memory. And then we can graph that in Grafana. We can put that in Influx DB and then Grafana can graph that for us. And then we can run this on the show here. You just have to do the initial login. So that pipeline is running already. So at this point, what it's doing is Jenkins is saying, okay, I know I have this pod template that has the Fedora 28 image. It's built. I want to deploy that and run this metrics.sh test on it to stress my CPU and my memory. At that point, you can get stats from Grafana not only on the metrics of the CPU and memory, but basically how long did it take your build and the pipeline build to complete? How many were successful, how many failed? You can get all that information from there. This just shows, again, the full stack that is up and running. Go to the cool stuff. So this is just showing that we're executing this. Basically every time out is 90, so it runs for 90 seconds to do the stress test. And it does it about five times. Initially, obviously, the data to show you wasn't that impressive. So actually what I did was I let the system run for over basically almost 48 hours to get more data to show that. But I'll show you the initial data that gets put out there in the... So now we can go to Grafana. You can see it's not as exciting because we did one run basically of this. So we had one build succeed. One little dot, obviously, in the last hour. But I have another video that kind of shows this running over a period of time. And if the network permits, we could also show this a little bit live, too. So let me go to... So this is the second video here. This shows that we've run 50 builds now. So now we have more of a data set to show. You could see, based on the last 24 hours of what was stressed out in the CPU and the memory, we have also to show the sample pipeline of how many runs we've run through that. 49, we're on the 50th right now. And we can show the 24-hour view of what that looks like. And that kind of gives you also an idea of how long did it take your builds to run? Was it faster during certain parts of the day? But this just shows a sample of what you can do with it. Your project may have a different target or different goal. This is what our target was just to show you kind of how all this stuff wraps together and using the different components, all running inside the new platform, which is OpenShift and Kubernetes. I do have another demo to show of Jacob's file runner and how he set all that up. But I'll leave that if we have time at the end for that. So that was basically the demo of how all this comes together. It's all maintained in two repos. The contract will be set up being the main repo. And then there would be your project repo. In this case, I had a sample project to set up. So the future, what does the future look like? Obviously, I mentioned APBs, and that's sort of future. It's good for... It's really good for deploying a configuration in OpenShift. It's not really for maintaining the lifecycle of it. That's kind of where you get into Helm charts or operators. You know, it's really a tool for, I would say, Helm is a tool for managing packages called charts, and it provides the following. There are three important concepts here. The chart, it builds information necessary to create an instance of a Kubernetes application. So it keeps... It's basically a builder or a packager for your Kubernetes application that's going to run. And then we get to operators. So operators are a little bit more involved. It's really a method of packaging, deploying, and managing the complete lifecycle of your Kubernetes application. You know, it also maintains its lifecycle so as you make changes, your operator will then control whether something gets redeployed or something is torn down, or it basically is like almost self-healing of an application in that sense, and it just manages it. It's kind of software to manage software in that sense. It's what it's been called. And then we get to kind of one of the new kids on the block, which is Knative, which is really kind of... It really extends the Kubernetes API. It provides a set of middleware components that are essential to build applications. You know, by having serving, which is you might have heard of serverless, that you can deploy an application on the fly via a CRD eventing. And the kind of part that comes back to CI and CD is really the build pipeline. So they actually have a component of this that is may fill in some of the gaps or take over some of the things that Jenkins does. That could be just native to actually Kubernetes itself. So this is actually Knative as an upstream project. You know, I recommend checking it out. I have links in the end of the presentation. You can contribute to it. I would say the key thing, too, it's just like source to image is OpenShift's version of taking source code and building an application out of it. This is kind of another way to do that and probably more upstream than even S2I is at this point or more widely used in S2I. So like I said, going back and kind of talking about Knative, this is kind of the setup. It does require if you're using serverless or serving an eventing, you need Istio as the mesh. It is source-centric and to deploy container-based applications. It can run anywhere. So any of the things that we're showing you, the platform OpenShift or Kubernetes, we can run this either cloud or third-party data centers or on-prem. And the idea, too, around the Knative stuff is to identify similar application patterns to deploy your application and really codify those best practices. So kind of round out the future of what we showed before is, like, today we have S2I templates, Dockerfiles, and JK shared libraries, which is great, but now as we look towards the future of other things that we could deploy as part of the setup that I showed you, this infrastructure, we could use APBs, you could set up Helm charts, the Knative templates that are available, or even operators. So to kind of show that box now is part of our infrastructure, we would have maybe we would deploy operators for ourselves that would help the infrastructure as well as Knative templates, or maybe your project also has some of these projects, these operators as well as Knative templates to use as well. The idea is that we want to make this platform flexible and that we can keep adding into it. You can deploy your own pieces into it. All you really need is the OpenShift platform with some ansible post hooks to actually do any extra stuff that you want to do after you've deployed it. So that's my links. I think we do have really only halfway through, so I do have some time to show you that other demo. And then we'll open it up for Q&A. So I wrote this script that basically pulls down the Jenkins file runner repo, builds the war file, or sorry, builds the package, the Jenkins file runner jar, and then at that point I can pull down the latest war file that exists from Jenkins, and I can insert my, inject my own plugins that I want into that, and then I can actually run a Jenkins pipeline, which you'll see at the end of this. This is just kind of doing some of the install. Here we are pulling down the war file. That was just a building of Jenkins file runner, and now we'll pull down the war file and then you'll see also how we inject the plugins into the system. At this point we had a list of plugins, and now we're actually installing this inside that in Jenkins home directory. So this is the file at the end. We're basically, this is what you would usually do in Jenkins, is Jenkins file runner command. This is pointing to the home directory of Jenkins that we built the plugins where the plugins are at, and then executing our Jenkins file. So that was basically it. We did an LS of just a shell step in a Jenkins pipeline. So instead of having a full blown Jenkins with the UI and all of its other persistent stuff that you need, you can actually run Jenkins right from the command line with the Jenkins file runner, and I just wanted to kind of show that kind of where Jenkins is cloud business headed with Jenkins in that case. And there's the pipeline file itself. That's it. So I'll open it up any questions about what I present that I know I cover a lot, and we can go back through anything that you need. Any questions? You're so impressed. Oh, the Jenkins file runner, or when I was showing? The base is actually the, it's the OpenShift Jenkins that's available upstream. Yeah. I don't think that's Fedora based though. Minishift is the overall platform running on. We're deploying a container that Jenkins is running on, which is based on OpenShift's version of that. That base is what allows us to configure Jenkins with any globals we want to set up, any of the plugins, all that stuff. So the same stuff I showed you with the Jenkins file runner of installing those plugins. OpenShift uses the same mechanism with the S2Y templating to do that. Any other questions? So the question is, can we, can you have an Amazon, a Kubernetes cluster on Amazon? Is that what you mean? Or, yeah. We could provision a cluster in Amazon through this, or we could talk to an existing cluster. We kind of focused on OpenShift or Minishift, which is probably a little different than this vanilla Kubernetes cluster. But there's no reason why you could not build an OpenShift cluster in AWS as well. Because as you hear, I used OKD, which is the open-source version of OpenShift anyway. Just the yellow part, which is... Yeah, exactly. In this case, I only set up tie to Jenkins. But there's no reason if you knew how to do it some other way, you just wanted to set up Grafana and FluxDB, you could deploy those templates your own way using our mechanism here, but it would be in your project and you can configure it any way you want. Are there any questions? All right. Well, thank you. Appreciate it.


Hello and welcome to this clip. Some of the deadliest clashes have been seen in Kashmir yesterday, after 11 militants were killed in three separate encounters carried out by the army. After these militants were killed, many protests emerged in the two districts where the killings happened, that is the districts of Anandnag and Chopian. So to discuss these developments and to discuss the other incidents that have been happening in Kashmir in the past few days, we have with us today Gautam Navlaka, who is a civil rights activist. So Gautam firstly talking about the clashes that have occurred yesterday. So we saw that we are seeing this huge support towards the militants from the civilians in Kashmir. After these people were killed, a lot of civilians came out to protect, to sort of shield the militants in the areas where these encounters were happening. So what is this atmosphere we are seeing in Kashmir today? Well, as far as the three encounters that you talked about, this is the first time and since 2010-11, I think, my memory serves me right, that there been such a mass casualty suffered by militants in a single day. So that by itself is a very significant loss for the militants. But the more interesting part of it is, as you pointed out, is despite operation all out, despite the threats and warnings issued by the armed forces, the army, the police, the CRPF, and the authorities at various times, people still come out and gather at a counter-site, shouting slogans in support of the militants, exerting them and doing everything to lend support to them and enabling them to also escape. This phenomenon, which began around 2013-14, and picked up after Burhan Muzzafarwani is killing in 2016-July, since picked up, and it shows no signs of abating. And it's in that context, if you look at the civilian casualties suffered yesterday in these encounters, it's pretty large. More than 200 people went to the hospital with injuries. A lot of them with bullets and a lot others with pellet injuries.  And it's this which also deserves to be taken note of that, yes, militants suffered a major loss in a single day, losing 11 of them. And by the way, they are all local youth. So the death of local people, the fact that civilians come out and continue to come out in such large numbers. I think it's a warning for the Indian government that the policy of military suppression is not going to work. Since this operation all out began, they've suffered a lot. Civilian killings have been on the increase. This year alone, roughly I think about 16, 17 civilians have so far died in these various encounters. It's just been three months. And just three months. And if you compare it with the number of militants who have died as well as the security force personnel who have died, it's pretty significant. And also, it's not like the militant numbers are going down. We're seeing a surge in the number of... Exactly. So the message also of civilians turning up at encounter sites is also that despite the fact that the militants get killed in encounters, in large numbers, there is no dearth of recruits to militancy. So at this level, this militancy can persist for a very long period. They don't require because it's the civilian support which is acting as a force multiplier for them. So that is, I think, a lesson that we should heed. Not the lesson that is being made out. I mean, people coming out and the army officers and all making this boastful claim that, well, we have dealt a major blow to the militancy and we'll soon bring it to an end or bring them to the knees, et cetera, et cetera. I think one should be more careful about declaring victory because there is very little that shows that it shows any sign of abating any anytime very soon. So the second major development in the state is the lifting of the house arrest of Sayed Ali Shah Gilani along with him. The other leaders of the Joint Resistance Leadership, Mirwez Farooq as well as Yasin Malik have also been given permission to carry out their social activities and political activities. So what sort of impact do you think this will have? Well, I think that the timing is pretty unfortunate for the government of India because if they believe that by releasing the three leaders, the three that comprise the Joint Leadership, Sayed Ali Shah Gilani, Mirwez Omar Farooq as well as Yasin Malik of JKLF, that they might be able to, that they were trying to send the message that, well, things are in their control. Actually what it shows is that they were compelled to release them because this policy of confining them to house arrest or arrest, ensuring that they don't come out in public, they don't hold rallies, they don't deliver speeches, et cetera, et cetera, would somehow bring the movement to an end. I think that has been belied. On the contrary, what has happened is the militancy picked up because when you close all other avenues, there are curbs on your freedoms and crackdown on all kind of protests and all, then you leave people with no choice but to end up not just owning the militants but also extending support to them as we have seen in the case of them turning up in large numbers at the counter-site. And with the Amarnath Yatra now due in June, the Anvil Amarnath Yatra, I think they had no choice but to release them to see whether it could bring the temperature down, so to say, in Kashmir. Well, it remains to be seen whether it actually results in that because they had also been, they have also been warned that while they have been released, they should not cause any law and order problem and not give in to any anti-national speeches and things like that, which is ridiculous because going by the parameters and set up by the BJP government, every statement itself can be considered as anti-national because any criticism of armed forces or of repression, of killings of civilians, lack of bringing the perpetrators to justice, etc. Anything can be construed as amounting to anti-national statements because it's directed against armed forces of India, etc. So I think it's pretty, but if they thought that by releasing them, they would be able to release pressure and bring the temperature down and maybe there would be a decline in civilian support for militancy, I think it's too early to say that. Also Dineshwar Sharma, I mean, he recently went on a visit to Thrall, I think. I mean, we're not seeing much resulting from his visit. Well, Thrall, it was reported by most of the Indian newspapers as though he went to the lion's den and was managed to meet people. Actually, the reality was altogether different. He entered an area where everything was shut down. There was heavy deployment of security forces and the usual suspects came to meet him. Nothing worthwhile came of it. So, I mean, his role, I mean, in any case, Government of India has declared on the floor of parliament that he was not meant to talk to anybody but to the representatives of people, which means those elected representatives. But those elected representatives have no quarrel with India.  They declare their allegiance to Indian constitution. They have no problem with it. The problem is with those who are questioning accession to India, who are talking about the right of self-determination. You have to reach out to them and talk to them. And there has been a miserable failure. So lastly, moving on to the situation in Jammu. I think we're seeing this shift in people's attitude towards BGP. Even after the Kathua case where BGP was supporting these locals who wanted the case shifted to CBI. Now, even these people seem to have sort of turned against BGP. Like we saw, the BGP's committee meeting was shifted from Kathua. So what can you tell us about that? Well, for too long, we have ignored developments in Jammu and one has treated whatever was happening in Jammu and Kashmir. I mean, it was focused on Kashmir as though it's unrelated, that whatever happens in Jammu does not impact or contribute to deterioration of the situation and conditions in Kashmir. Now, it's become evident that actually one can't talk about Kashmir but also simultaneously talking about Jammu, which is in the midst of a deliberate attempt to create a communal polarization, including encouraged elements which speak of ethnic cleansing, getting rid of Muslims from the Hindu dominated areas. And even the muscular talk about Pakistan and teaching Pakistan a lesson and all, which swayed a lot of people who stayed close to the line of control or the international border with Pakistan. We are now seeing that signs of people actually being frustrated with BGP because they had expected something to change, to transform peace, to return to an area where the fields are so that they can carry on tilling the land and take care of the livelihoods, school education, etc. of the children uninterrupted by shelling and artillery exchange of fire between Indian and Pakistani troops. It's the opposite that has happened. Things have become worse. From firing bullets, now they are firing heavy artillery guns against each other, causing far greater damage than one had expected. So there is a sense of frustration with BGP. The frustration is also amongst those hardened Hindutva elements who feel that the BGP is not backing them in their Hindutva project. So this decision to move the state executive meeting, as you pointed out, from Kathwa to Suchedgarh, they realized that if they had held it in Kathwa and a protest had taken place while the state executive meeting was going on, they would have sent a wrong message to their own constituency. Having created this communal monster, now they find that it's demanding a pound of flesh, which they are not in a position to deliver. They can't deliver on the demand for ethnic cleansing, for instance, of Kathwa and other districts where the Hindus are in large majority. They can't deliver on a peaceful line of control and international border. Naushara, for instance, has been having more than 40-day-long agitation that went on there because they had promised that Naushara would be declared a new district. But they were unable to do anything about it in the last three and a half years. Of course, this is also coming from, as you've seen, this new parliamentary committee report which shows that only 22% of the 80,000-curve package that was assigned for G&K has been spent. Yes, although I must also add at the same time that BJP's or Prime Minister Narendra Modi's famous economic package is not the only package that has suffered. Almost all packages announced by successive Prime Ministers in the last 30 years have all failed to deliver on the promise. But it is true that BJP's performance has been miserable. To be able to only release in the last three years, 22% of the funds out of 80,000 promised that they were not even serious about what they had declared. If you remember two years back when Mufti Sahib was still alive at a public meeting after Mufti Mohammed Sayed had spoken and urged Prime Minister to reopen dialogue, resume dialogue with Pakistan and hold talks with Hurriyat and others, he had turned around and snubbed Mufti Sahib by saying that he did not need anybody's advice on Kashmir. But it seems this government and its Prime Minister actually needs a lot more advice and it's high time they start paying heed to advice of people who know what the situation is on the ground and this make-believe world that you can through military suppression bring situation under control showing that it's not going to be like that. When people are against, people are disenchanted and frustrated and there is no political resolution inside. There is no way you can bring either militancy or this movement to its new. It's impossible. So thank you Gautam for joining us in this discussion and thank you for watching this clip.