tag:blogger.com,1999:blog-47857094426370444342024-03-14T03:02:58.123+05:30Jay's BlogRandom stuff I give a damn aboutJay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.comBlogger20125tag:blogger.com,1999:blog-4785709442637044434.post-62886796467269817372018-08-30T00:53:00.000+05:302018-08-30T00:53:59.875+05:30New Website!You can find me at my new website over at <a href="https://www.jaybosamiya.com/">https://www.jaybosamiya.com/</a>.<br />
<br />
At the moment, my plan is to maintain work/research/security/etc related blogposts on that website. I will <i>not</i> be removing those blogposts from this blogspot website, but will no longer be publishing those here. Go over there to all my latest blogposts, and a regularly maintained list of ways to contact me.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.comtag:blogger.com,1999:blog-4785709442637044434.post-65718399856082093072018-05-31T02:35:00.000+05:302018-05-31T04:36:25.557+05:30My Awesome Experience at the Summer School on Formal Techniques (SSFT'18)I spent the past week, at the <a href="http://fm.csl.sri.com/SSFT18/">Summer School on Formal Techniques</a>, and it was an absolutely amazing experience. Chronicled below, are the different great talks/labs that were part of this week long program, as well as my thoughts interspersed in. Overall, this was an unforgettable week, where I learnt a lot, made new friends, and had some nice discussions about a lot of very interesting topics. I also found out about some things that I had no idea about before, and thus I decided to write at least a short summary down for each of the different things that happened, so that maybe it might be useful to some (or more likely me from the future) as references for things to read up on.
<br />
<br />
<table align="center" cellpadding="0" cellspacing="0" class="tr-caption-container" style="margin-left: auto; margin-right: auto; text-align: center;"><tbody>
<tr><td style="text-align: center;"><a href="http://2.bp.blogspot.com/-IUtvYbolgoE/Ww8PJljGawI/AAAAAAAALtA/sv-AYAg7fBotTHu8F0U_k-TXaybCk_gdgCK4BGAYYCw/s1600/2018-05-22%2B17.51.22.jpg" imageanchor="1" style="margin-left: auto; margin-right: auto;"><img alt="Group Photo" border="0" height="265" src="https://2.bp.blogspot.com/-IUtvYbolgoE/Ww8PJljGawI/AAAAAAAALtA/sv-AYAg7fBotTHu8F0U_k-TXaybCk_gdgCK4BGAYYCw/s400/2018-05-22%2B17.51.22.jpg" title="" width="400" /></a></td></tr>
<tr><td class="tr-caption" style="text-align: center;"><span style="color: #0000ee;">Group Photo at SSFT'18<u><br /></u></span></td></tr>
</tbody></table>
<br />
I initially heard about SSFT via a message on our <a href="https://project-everest.github.io/">Project Everest</a> Slack. After all, two of our team (<a href="https://www.microsoft.com/en-us/research/people/nswamy/" target="_blank">Nikhil Swamy</a> and <a href="https://jonathan.protzenko.fr/" target="_blank">Jonathan Protzenko</a>) were going to give talks and conduct tutorials at this summer school. Since I had only recently (approximately a year ago) started my journey into Formal Methods/Techniques, this seemed like the perfect opportunity to widen my field of view in this field- a field which seems to be able to cover almost every topic known in Computer Science. As a person who started from a more "systems-y" background, I (rightly) thought that this would give me the requisite theoretical background to dive deeper into this field, in addition to giving me practical hands on experience with other tools and techniques used in this field. I'd been using <a href="https://fstar-lang.org/">F*</a> for almost a year by now, but had yet to have had a chance to mess around with other tools that are commonly used (except for <a href="http://research.microsoft.com/dafny">Dafny</a>, which is a beautiful language to start off in this field btw). The fact that approximately half the time was dedicated to the labs, surely was a bonus!
<br />
<br />
The Summer School was held at Menlo College in Atherton, California, from Sat May 19 to Fri May 25, 2018. I must thank <a href="http://fm.csl.sri.com/">SRI</a> for organizing it, and NSF for funding our travel/stay/etc. The organization of the entire summer school, as well as how everything was managed, was absolutely impeccable. Oh, and a special shout-out goes to the chefs at Menlo College who made absolutely marvelous food that kept us powered up through this week long intense mental workout!<br />
<br />
As for the actual summer school, it started off with an optional background course, titled "Speaking Logic", which ran over the first two days (i.e. Sat/Sun). Despite it being optional, it seems like most of us at the summer school attended it, and it definitely was worth it. <a href="http://www.csl.sri.com/users/shankar/">N Shankar</a> took us through a beautiful journey through the fundamentals and principles of logic and formal methods. Along this journey, we made stops along Naive Set Theory, Propositional Logic, Cook's Theorem, Reductions to SAT, Proof Systems, Minimal Logic, and Meta-Theorems. We also stopped off at Interpolation, Resolution, First Order Logic, SMT Solving, the Tarski-Knaster Theorem, and Bounded Model Checking. Alongside these (already amazing) topics were the awesome detours that Shankar took, with his own anecdotes and stories. A bunch of these even led to some intense discussions during and after the lectures! We did do a bunch of proving things in <a href="http://pvs.csl.sri.com/">PVS</a>, and it definitely seems like a great tool to get people started with some serious formal proofs :)
<br />
<br />
After this deep dive into Logic, <a href="http://www.lix.polytechnique.fr/~lengrand/">Stéphane Graham-Lengrand</a> took us on an adventure through Type Theory, where the Proofs-as-Programs paradigm reigns king. Type Theory is the foundation for a wide variety of interactive theorem provers, such as <a href="https://coq.inria.fr/">Coq</a>, Agda, Lean, Matita, etc. During this talk, we went over the Lambda Calculus and Simple Types, Intuitionistic logic (and Constructivism), Computing with Intuitionistic proofs, HOL with proof-terms, Dependent types, and more, all building up to the final bomb that blew our minds- Homotopy Type Theory. Stéphane used an extremely well thought out analogy, using a Vacuum Cleaner Power Cord, to explain the basics and motivation for Homotopy Type Theory (HoTT). I'd always wondered why people were excited when talking about equalities, but with just this one example, Stéphane has ensured that I am definitely going to dive into this topic, much deeper, sometime soon! BTW, this entire talk was punctuated with proofs done in Coq, and the exercises for the same, can be found <a href="http://www.lix.polytechnique.fr/~lengrand/SSFT2018/">here</a>.
<br />
<br />
As day 2 came to an end, some of us realized that we'd covered a <i>lot</i> of ground, and that we'd need some time to digest it, so we went back over our notes and the slides, trying to ensure that we'd actually got some of the details straight. BTW, the speaking logic <a href="http://fm.csl.sri.com/SSFT18/speaklogicV8.pdf">slides</a> are not only available online, but are also quite detailed, and I would recommend the interested reader to take a look at these to get an overview of what logic and proofs and formal methods are about. However, the slides do not include all of those amazing anecdotes etc, that were there during the actual talk, so maybe you should consider joining the summer school when it happens next? ;)
<br />
<br />
Starting from Day 3 (i.e. Monday), we had a change of pace, with the schedule changing to a bunch of talks until mid-afternoon, followed by a couple of lab-sessions.
<br />
<br />
Monday's talks started with a wonderful talk by <a href="https://homes.cs.washington.edu/~emina/index.html">Emina Torlak</a>, about <a href="https://emina.github.io/rosette/">Rosette</a>. The talk, titled "Solver-Aided Programming" was about a programming model that integrates solvers into the language, which provides constructs for program verification, synthesis, and more. A strong emphasis was placed on the paradigm of "Verify, Debug, Solve, Synthesize", which are implemented in Rosette as powerful user-friendly constructs. Since Rosette is built on top of Racket, we get all the benefits of Racket (and thus, all the LISP goodness), which leads to a very elegant way to program using solvers. The four parts of the paradigm can be thought of as the following queries that any user might want to ask a language: (1) Verify: "find me an input on which the program fails, or prove that it cannot fail", (2) Debug: "localize the bad parts of the program", (3) Solve: "Find values that repair this failing run", and (4) Synthesize: "Find code that repairs the program".
<br />
<br />
The next talk was by <a href="https://www.microsoft.com/en-us/research/people/nswamy/">Nikhil Swamy</a>, about <a href="https://fstar-lang.org/">F*</a>. It explained how there is a gap between interactive proof assistants (such as Coq) and semi-automated verifiers of imperative programs (such as Dafny), and that F* was about bridging that gap. F* has an ML-like syntax, and has dependent typing. What this means is that verification is done via the process of type checking. The rest of the lecture continued with examples showing (simple) proofs written in F*, for functional programs, as well as a discussion on how we can write proofs for effectful code, using Monadic effects, and by modeling the heap. Personally, despite having worked with F* for almost a year now, I still gained some new insights, such as the fact that subtyping being possible due to the core feature of refinements being proof irrelevant after finishing the proof.
<br />
<br />
Next up, after lunch, was a talk by the unforgettably energetic <a href="http://www.math.tau.ac.il/~msagiv/">Mooly Sagiv</a>, titled "Modularity for decidability of deductive verification with applications to distributed systems". It took us through the motivation of why decidability was crucial for verification, and that despite seemingly restrictive (since the logic then becomes less expressive), we are able to talk about and prove whatever interesting properties that are needed, at least in the case of distributed systems. Specifically, this decidable deductive verification was demonstrated using <a href="http://microsoft.github.io/ivy/">Ivy</a>. The basic idea behind this is that when a verifier goes into the "Unknown" state (i.e., it is divergent; aka "I can't decide"), this gives very little (if any) information back to the person working with the verifier, since the property being verified might either be true, or might have a counter-model (read: counter-example), but no further information is known. Instead however, if we were to restrict ourselves to a logic that is always decidable, then we are guaranteed never to reach the "unknown" case. The talk then went on to some examples of verification in this decidable world (and how to represent some things that are "not expressible", but turn out to be expressible when you look at them from a different perspective). What was <i>really</i> interesting was how many fewer lines of proof were required per line of code in Ivy, in comparison with other tools. More details about how it is able to do so, would be in the following lecture.
<br />
<br />
After a short break, we had the lab sessions, where we split off into 2 groups (using a great way to introduce randomness btw: if the first letters of both your first and last name lie in the same half of the alphabet, then you belong to group A, else group B). All the groups had all the lab sessions, just in a different order; since I was in Group A, my order shall be based off of that.
<br />
<br />
Our first lab session was by Emina Torlak, where we got to dive into working with Rosette. As a warmup, we worked on finding and fixing a bug in a tiny BitVector example. As a larger example, we worked on Sudoku. Starting only with a checker (i.e., a program that, given a Sudoku solution, results in a "yes it is a valid solution" or "no it is not"), we turned it into a Sudoku solver (find a solution, given a puzzle), a validity checker (checks if a Sudoku puzzle has exactly 1 solution), and minimal puzzle generator (a puzzle that has the least number of constraints needed to be valid). What was extremely interesting was how easy it was to build each of these using just the checker. Rather than gain domain knowledge about how to write solvers, generators etc., we simply piggy-backed on the already implemented checker, and with only a single-digit number of lines of code, were able to implement all of this! Unfortunately, I do not know of a public link where this tutorial is available, but it is a <i>very</i> well designed and thought out tutorial that I'd recommend people try if they can find it.
<br />
<br />
Next up was the lab session by Mooly Sagiv, about Ivy. Here, he gave a live demonstration of using Ivy to verify a protocol for mutual exclusion. In contrast with previous experiences with verification, this was a welcome change, where the tool itself gives you a graphical counter-example, when it is unable to prove that a certain invariant holds. While it still falls upon the user of the tool to provide stronger invariants that can be proven via the induction, being able to see these counter examples instead of simply a "timed-out" as is more likely in other tools, is definitely a game changer
<br />
<br />
The next day (Tuesday), we started off with a talk by <a href="http://www.cse.chalmers.se/~abela/index.html">Andreas Abel</a>, about <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php">Agda</a>- the dependently typed functional programming language which is a proof assistant. The material for what was covered can be found <a href="http://www.cse.chalmers.se/~abela/ssft18/index.html">here</a>. The talk had a strong "do this live" approach, where Andreas was explaining things as he continued working on Agda code, proving things. We also went over an elegant representation and ordering invariant for binary search trees in Agda. This was based off of Conor McBride's paper <a href="https://dl.acm.org/citation.cfm?doid=2628136.2628163">"How to keep your neighbours in order"</a>. Personally, I found that Agda had a <i>very</i> elegant interface which made it more natural to think about proofs, and this made understanding the proofs themselves a <i>lot</i> easier.
<br />
<br />
The next talk was by Emina Torlak. Yes, almost every speaker gave 2 talks and had 2 lab sessions. This time, the talk was about how to build a solver aided language. The classic (read: <i>hard</i>) way to build such a tool is to build a symbolic compiler, which requires an expertise in Programming Languages, Formal Methods, and Software Engineering. A much easier method would be to build an interpreter for the language, and have something that uses this to build all our tools for us. This kind of tool is a significant technical challenge and is what Rosette solves for us. We can simply have a (deep or shallow) DSL hosted in Rosette (where, since Rosette is built on top of Racket, this becomes very easy), and then we can easily build the 4 tools- verify, debug, solve, and synthesize, very easily. The talk then went into details about how this massive technical hurdle is overcome (since neither symbolic execution, nor bounded model checking, are up to the exact requirements of this task of precise symbolic encodings). It is done via type-driven state-merging. This was followed by 3 different use-cases (out of many many others) where Rosette has been used to get some very interesting results.
<br />
<br />
The last talk before the break before the labs, was by <a href="https://jonathan.protzenko.fr/">Jonathan Protzenko</a>, titled "Verified low-level programming embedded in F*". Specifically, the talk was about a low-level subset of F*, named Low*, which allows one to write and reason about low-level C code. The talk goes into detail about how different parts of C are modeled in Low*, as well as talks about the kreMLin compiler, which compiles Low* code to readable C. Since proof-erasure is a part of this process of compiling down to C (because C has no notion of proofs by itself), we only need to use the low-level subset in the actual computation bits, and can use the full power of F* in the proofs. There is a tutorial for Low* available <a href="https://fstarlang.github.io/lowstar/html/">online</a> (currently a work-in-progress).
<br />
<br />
The first of the labs on the same day was part 2 of Emina Torlak's lab. In this, we worked on actually building DSLs- first a shallowly embedded DSL, followed by a deep embedded DSL, for a circuit-based programming language. An important thing to note here is that shallow DSLs are faster and easier to implement, and are almost always the right choice for either the "verify" or the "debug" operations. However, if we want any sort of "synthesize" operation, then shallow DSLs fall short extremely quickly, and deep embeddings work out <i>much</i> better.
<br />
<br />
The second lab on Tuesday was part 1 of the F*/Low* Lab, conducted by Nikhil Swamy. Here, we went across some select examples from the <a href="https://www.fstar-lang.org/tutorial/">F* Tutorial</a>. Special emphasis was placed on how one comes up with these proofs, and how F* is able to infer most of the proof, requiring only a "here's the form of the induction" argument. One interesting point that came up during this discussion was the possibility for F* to automatically "guess" the form of the induction. This seems quite doable in a large number of cases, and is something that is worth considering, though F* doesn't support this at the moment, and one needs to explicitly point out things like "do an induction on this list" (and the rest of the proof is automatic). The tutorial is well written and thought out in a way to be self-contained, while not repeating concepts that might be known to an OCaml / F# developer. There are some nice motivating examples/stories in the tutorial online too. I would definitely recommend the interested reader to try these out (though some people might need to take a crash course on OCaml / SML / F# syntax, if they aren't used to it).
<br />
<br />
With this, Tuesday came to a close, and we started Wednesday with a talk by <a href="https://www.sosy-lab.org/people/beyer/">Dirk Beyer</a>, about <a href="https://cpachecker.sosy-lab.org/index.php">CPAChecker</a>. The <a href="https://www.sosy-lab.org/Teaching/2018-SummerSchool-SSFT18/">talk</a>, titled "Configurable Software Model Checking - A Unifying View" was about how one can unify different techniques, ideas, and algorithms in program analysis and verification, into a single framework, that also allows for the creation of "intermediate" algorithms. This ability to configure allows one to move all the way between imprecise but scalable Data-flow analysis, all the way to the precise but expensive Model Checking, by better combination of abstractions. Via Dynamic Precision Adjustment, one gets a better fine tuning of abstractions and gets adjustable precision, thereby allowing a similar movement between precise/expensive and imprecise/scalable. By using an adjustable block encoding, one can change how many statements are handled together all at once. The rest of the talk revolved around CPAChecker's features, concepts, ideas, algorithms, as well as architecture. We'd get to play around with it in the lab soon! Oh, and btw, CPAChecker has regularly been doing well in the <a href="https://sv-comp.sosy-lab.org/2018/results/results-verified/">SV-COMP</a> Competition on Software Verification, coming in with Gold in 2018!
<br />
<br />
Next up, part 2 of Andreas Abel's talk. He continued with the "doing it live" approach, but this time, we were looking at examples from programming languages, like representation of expressions, evaluation, and equational reasoning. Again, the files can be found <a href="http://www.cse.chalmers.se/~abela/ssft18/">here</a>. In my opinion, understanding these things well definitely involves following along, proving these things in Agda, so I would 100% recommend interested readers take a look at the <a href="http://www.cse.chalmers.se/~abela/ssft18/lec2/Lec2.zip">Lec2.zip</a> file on the website, and try proving stuff. The comments in these files are <i>really</i> helpful, especially if you've already gone over the files from Lecture 1. I have to specially point out how amazing it is that time was put in to make sure these examples were extremely well documented, and is thus easy enough for a beginner to follow along. Being at the talk though helped a lot too, and probably saved a bunch of time for many of us in understanding these ideas.
<br />
<br />
And then right after lunch, part 2 of Mooly Sagiv's talk. This time, the talk was much more about the technical details of Ivy and its 3 most important principles: (1) What 1<sup>st</sup> order structures would exist in the language -- abstract states and imperative updates. This gives us a "step towards decidability". (2) Theories as add-ons. When the user axiomatizes domain knowledge in EPR (which is what gives the decidability), soundness is checked, and we get reusable domain knowledge with predictable automation. (3) Modularity for breaking quantifier alternation cycles. It falls upon the user to break these cycles, and Ivy will only point out that there are cycles, instead of trying to break them by itself. One very interesting idea that falls out of this is how sometimes it becomes useful to perform the abstraction of functions as relations instead.
<br />
<br />
As for the labs for Wednesday, we started off with the first of the Agda labs, by Andreas Abel. In this lab, we worked on some simple definitions and proofs in Agda. I'd strongly recommend going over the <a href="http://www.cse.chalmers.se/~abela/ssft18/lec1/Exercises1.agda">exercises</a> which are quite self-contained, and have some interesting bits that one might get stuck upon before realizing where to go next.
<br />
<br />
The next lab was the first of the CPAChecker labs, by Dirk Beyer. Here, we followed along parts of the <a href="https://masp.gitlab.io/CPAcheckerTutorial/">CPAChecker Tutorial</a>, which is also very self-contained. It contains a bunch of nicely chosen examples which help in identifying different features of CPAChecker, and has a nice progression to it.<br />
<br />
And with that, Wednesday draws to an end. By now, we've all had a lot of interesting ideas, works, thoughts, anecdotes, stories, and concepts explained to us- and while for some, it might have seemed like an overwhelming amount, to most of us (or at least to me), this was a treasure trove of knowledge in a short, condensed, concentrated form. Personally, I was having an amazing time here. I must also bring up the fact that the rest of the students at the summer school were also a major factor in this, since everyone was brimming with ideas, and worked on such varying topics, that no matter who you were talking to, there was always something amazing to learn.
<br />
<br />
Anyways, back to the talks- we are now on Thursday. We start the day with a talk titled "Verifying Properties of Binarized Deep Neural Networks", by <a href="http://narodytska.com/">Nina Narodytska</a>. With Machine Learning (and more specifically, Deep Neural Networks) becoming the rage and the norm for a lot of industries, it becomes essential to actually try to understand properties about them, especially about robustness to perturbation. In this talk, a specific class of neural networks is taken and is studied via an encoding to Boolean Satisfiability (i.e. SAT). Once it is encoded at a SAT problem, one can then leverage the full-power of research done in making better SAT solvers, to be able to scalably verify properties of these binarized deep neural networks. An arXiv pre-print of the work can be found <a href="https://arxiv.org/pdf/1709.06662.pdf">here</a>.
<br />
<br />
Next up was the second talk by Dirk Beyer, which was split into 4 parts (again, the material can be found <a href="https://www.sosy-lab.org/Teaching/2018-SummerSchool-SSFT18/">here</a>). One of the parts was about how one might combine different verifiers etc. Currently, we have a lot of verifiers, due to competitions such as SV-COMP, but it would be great to be able to leverage the strengths of one to help the other. This is where conditional model checking comes in. A really elegant "reducer" based construction was shown, which allows one to basically "import" any verifier and make it use the results of a previous conditional verifier. Another part was regarding verification with witnesses, which was about witness validation, as well as stepwise refinement of witnesses. This is another case where multiple verifiers could work in conjunction to either aid each other, or to provide higher assurance in each other's results. Another idea was about execution based validation of witnesses- this one is especially important when talking to people outside of the verification community, since they respond best to "here's a test case that breaks the software" rather than "here's a set of paths which might lead to a break in the software".
<br />
<br />
Finally, the last of the talks of the day was by <a href="https://en.wikipedia.org/wiki/Gordon_Plotkin">Gordon Plotkin</a>. This talk, titled "Some Principles of Differentiable Programming Languages" was an absolute beauty! In this talk, he walked us through what Differentiable Programming Languages are, and why they are necessary (as well as difficult). He then went on to explain some previous foundational work that might have been useful, if it weren't for those pesky partial functions. Following along, he went along his thought process in how he worked on designing the right language which has differentiation as a fundamental operation in it (despite having conditionals and looping). Personally, I found it extremely fascinating to see the thought process of reaching such an elegant language in the end. It starts off extremely messy, and keeps getting messier until suddenly, beauty emerges at the end. There are a whole bunch of notes that I wrote down during this talk, but I believe nothing can do justice to summarizing this talk. It was filled with lots of interesting side-notes, and anecdotes, and ideas that themselves could be talks of their own.<br />
<br />
Back to the labs: we started Thursday's lab session with part 2 of the Ivy lab, by Mooly Sagiv. At this time, we got to actually play around with and truly understand the though process behind coming up with inductive invariants while proving things in Ivy. We specifically took up the example of leader election in a ring, and tried to prove that at the end of the protocol, exactly one leader would be elected. Due to Ivy's fast turn-around time to respond to the written invariants, as well as its relatively easy to understand graphical representation of counter examples, it became much more about identifying stronger and stronger properties that might help us in proving the property we want, rather than fighting with the prover, which seems to happen in a lot of automated proof systems. At the end of finding the proof, we also end up having a very nice birds eye view of the proof, since we've written these nice inductive invariants, by the time we are done.
<br />
<br />
Next lab for the day: part 2 of the F*/Low* Lab, conducted by Jonathan Protzenko. Here, we were proving correctness and some properties of some short examples about working with machine integers, references, and buffers. The <a href="https://fstarlang.github.io/courses/fstar-sri-2018/LabSession.fst">code</a> which we were working on, is heavily commented, and is extremely easy to follow along after the F* tutorial. I personally would recommend doing it, to quickly get a handle on the basics of Low*. These examples however, should soon become a part of the (currently work in progress) <a href="https://fstarlang.github.io/lowstar/html/">Low* Tutorial</a>.
<br />
<br />
Next up, the Banquet. Everyone had an awesome time at this. And here's a picture of almost everyone who was there (looks like some people are missing from the photo, probably because the photo was taken very close to end of day):
<br />
<br />
<table align="center" cellpadding="0" cellspacing="0" class="tr-caption-container" style="margin-left: auto; margin-right: auto; text-align: center;"><tbody>
<tr><td style="text-align: center;"><a href="http://2.bp.blogspot.com/-yFEhO9EO5tM/Ww8RI7ItlaI/AAAAAAAALtY/chKVdCkzcEkhsyKro6HKErlvkIAQOAdoACK4BGAYYCw/s1600/2018-05-24%2B23.31.11.jpg" imageanchor="1" style="margin-left: auto; margin-right: auto;"><img alt="Group Photo" border="0" height="266" src="https://2.bp.blogspot.com/-yFEhO9EO5tM/Ww8RI7ItlaI/AAAAAAAALtY/chKVdCkzcEkhsyKro6HKErlvkIAQOAdoACK4BGAYYCw/s400/2018-05-24%2B23.31.11.jpg" title="" width="400" /></a></td></tr>
<tr><td class="tr-caption" style="text-align: center;"><span style="color: #0000ee;">At the Banquet<u><br /></u></span></td></tr>
</tbody></table>
<div style="text-align: center;">
<br /></div>
<br />
Finally, we arrive to the last day of the summer school (did a whole week go by so fast?!). We start off the day with 2 lab sessions (yep, labs instead of talks at the start of the day).
<br />
<br />
The first was part 2 of the CPAChecker lab, by Dirk Beyer. Here, we continued with the <a href="https://masp.gitlab.io/CPAcheckerTutorial/">tutorial</a>, but this time instead, we concentrated on the parts about combining verifiers, and about witness generation/checking. Personally, I found the reducer generating (arguably) readable code, which was interesting (and unexpected). Overall though, this lab helped cement the ideas that were discussed in the second talk by Dirk.
<br />
<br />
The second was part 2 of the Agda lab, by Andreas Abel. This time, we looked over more definitions and proofs in Agda (see <a href="http://www.cse.chalmers.se/~abela/ssft18/lec2/Exercises2.agda">Exercises2.agda</a>). In the course of this, we also ended up learning about various proof styles that are possible in Agda, especially when talking about auxiliary "helper" lemmas. Proving decidability of various things was a nice exercise and is something I'd definitely recommend trying.
<br />
<br />
As a fitting end to the summer school, was a talk by <a href="https://ptolemy.berkeley.edu/~eal/">Edward A. Lee</a> titled "What Good are Formal Methods?". Based loosely around his book, titled <a href="https://mitpress.mit.edu/books/plato-and-nerd">"Plato and the Nerd"</a>, he walked us through the nuances of how combining different deterministic systems can lead to non-determinism, and how moving between the viewpoints of a scientist and an engineer is essential in looking at the right way at models. Everything we say about, and prove about systems, is always actually about a model of the system, and depending on the viewpoint, either the model is flawed (scientist), or the system/realization is flawed (engineer). He then goes on to talk about non-falsifiable theories, with the "Digital Physics" hypothesis taken as a prime example. another interesting direction was about the Incompleteness of Determinism, which he shows via the concept of "Superdense Time". This talk was definitely an amazing journey through a lot of different ideas and concepts from a variety of different fields, that we do not even think about on a regular basis. I am definitely going to read the book, because if it is anything like the talk, it should definitely be a joy to read!
<br />
<br />
And finally, we come to the end of this brilliant, beautiful and amazing week. I got a chance to meet such awesome people, discuss mind-shattering ideas, talk about random topics in great depth, and make some great new friends and acquaintances. I hope to stay in touch with as many of you as I can, and hope to meet again sometime really soon!
Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-50674832312167902582017-07-04T18:37:00.001+05:302017-07-04T18:37:56.618+05:30A Story to Tell : My Experience at IIT Roorkee<span style="font-size: x-small;">[This was <a href="https://web.archive.org/web/20170702173537/https://expectationsiitr.com/experiences.html" target="_blank">originally published</a> on <a href="https://expectationsiitr.com/" target="_blank">Expectations IITR</a>, run by <a href="https://geekgazette.org/" target="_blank">Geek Gazette</a>, just after completing my B.Tech. at IIT Roorkee]</span><br />
<br />
<table align="center" cellpadding="0" cellspacing="0" class="tr-caption-container" style="margin-left: auto; margin-right: auto; text-align: center;"><tbody>
<tr><td style="text-align: center;"><a href="https://2.bp.blogspot.com/-fiyNpH8lVi0/WVuR3AaNFyI/AAAAAAAABnE/QHGCCdEj6-MbatidS6wuQ8GNRZo1ZwoTQCLcBGAs/s1600/Jay.jpg" imageanchor="1" style="margin-left: auto; margin-right: auto;"><img border="0" data-original-height="1142" data-original-width="1600" height="285" src="https://2.bp.blogspot.com/-fiyNpH8lVi0/WVuR3AaNFyI/AAAAAAAABnE/QHGCCdEj6-MbatidS6wuQ8GNRZo1ZwoTQCLcBGAs/s400/Jay.jpg" width="400" /></a></td></tr>
<tr><td class="tr-caption" style="text-align: center;">My desk is definitely not this organized</td></tr>
</tbody></table>
<br />
Truly, time flies extremely fast when you are enjoying yourself. These 4 years have been amongst the most memorable ones in my life till date, and have helped me grow as an individual in countless ways. First year was the first time I was staying away from home, for an extended period of time. To make things more challenging, I was at the same school for the previous 12 years! To come to a new place, and not a single familiar face to be found on campus, I definitely was anxious before arriving on campus. But my fears were unfounded, and I quickly found out, that in a campus with thousands of people, there are bound to be those who think alike, and we tend to find each other as time passes.<br />
<br />
Amongst my neighbours and branch-mates, I found friends whom I could go for trips and treks with. And since I had a massive collection of movies and TV shows that I'd brought from home on my laptop, frequent marathons were bound to happen. At the time, RJB didn't have a good internet connection (NoLAN, as we liked to call it), and so we ended up purchasing an Ethernet switch, and long LAN cables, so that we could all play Counter Strike. Even then, it was often more fun to just move chairs into a single room, and continuously curse while shooting in either de_dust2 or $1000$. <br />
<br />
Soon enough after joining IITR, different campus groups started their recruitment sessions. After asking around, doing some reading, and understanding what the different groups do, I decided to apply to only two -- Geek Gazette and SDS PAG. GG was a place for the geeks of the campus to unite, and try to change the world, one bit at a time. As I had tried writing short stories in the past, I applied as an editor to the magazine. It was during the interviews that I realised, that I had found my kind -- people who are extremely (almost obsessively) passionate about gaining knowledge about the things they love, and like to share those things with the world. Over time though, for me, it grew into a family where I could implicitly trust everyone in it. Other than GG, I applied and got selected into SDS PAG, which seemed like an obvious choice for me, since I had already been doing competitive programming since class 11 (Informatics Olympiads etc). Here was a place I found people like me, who lived on the "adrenaline rush" of solving puzzles and challenges through the use of logic, algorithms, and code. <br />
<br />
Academics, of course, went on, alongside all these amazing things, but overall, I didn't find it too much of a burden. As long as I stayed awake in class, I was able to manage great grades without needing to spend too much extra effort outside of class. And the great thing was, we only had ~25 contact hours a week, which meant that I could do a lot more than just merely academics. Hence, apart from all that I was doing, I decided to take a shot at open-source development. One of my seniors had said "doing a Google Summer of Code in first year is impossible", and I just couldn't accept this as true. After a few months of intense work, I got selected into, and that is how I spent most of my summer after 1st year (and the first couple of months of 2nd year) -- working on the open-source network security scanner, Nmap. It was an amazing experience, and I got to work with some of the most amazing developers and security enthusiasts. Even though it was not required, it was so much fun that I was spending over 70 hours a week! <br />
<br />
In a few months though, once the GSoC period was complete, I realised how tiring pure development could be. Additionally, 2nd year had begun, and with it, came a whole bunch of new hobbies. This is when I first heard of CTFs -- a Capture The Flag contests, where many challenges are given to hack into, legally. This seemed like awesome fun, and with a few friends, I decided to try it out. Little did I know, at the time, how important this would turn out to be. Soon enough, we were starting to get relatively decent at this "new" field, and we started taking part in national level competitions -- our first, being Deloitte CCTC, where we went and won! The thrill of breaking into software was something my teammates and I got addicted to, and over time, it decided the fate of our careers. However, at the time, it was merely a hobby. <br />
<br />
As a serious career prospect, I was considering research in Computer Science, but was unsure of the sub-field. One of the professor's course was really fun, and I decided to ask him for some research project work. Prof Bala suggested that I work with him, and Prof Partha (who had newly joined the department), on a topic in Image Processing and Computer Vision -- Scene Text Segmentation. This led me on a long journey of actually learning what research entails -- lots and lots of failed attempts, and that one final satisfying"Aha!" moment. It was great, and for the 2nd year summer, I decided to apply for foreign university internships in the field. Maybe it was bad timing, or maybe I needed to learn more, or maybe... -- whatever the reason -- I was met with mainly unanswered emails, and the occasional rejection. I took these rejections, at the time, as a way to have some extra focus on the project at hand. Over the course of the summer, with more improvements, I was able to obtain publishable results, and decided to write a research paper about it. It was accepted at the Asian Conference on Pattern Recognition, and I ended up travelling to Malaysia in the 3rd year to present it. That trip was amazing, and I still tend to use one of the photos clicked there as a profile picture on some websites. <br />
<br />
As part of enjoying life though, I think my friends and I had matured by then, and had started going for longer treks, and started playing "serious" games such as AoE2. Of course, a trebuchet is the weapon of choice to lay a siege with, since it utilises a counterweight to launch a 90kg projectile over 300m! Obviously, it is superior to the measly catapult, but I digress.<br />
<br />
By the time 3rd year rolled around, I was made the president of GG, and with that, came a whole slew of new experiences and responsibilities. I was able to lead an amazing team, with great friends by my side. Frankly, it was something I thoroughly enjoyed. It did take up basically all the time I had available, but I still managed to get a lot of other things done too. One of these, was to start up a new group on campus for security enthusiasts like me. This was the birth of SDS InfoSecIITR -- a group conducive to hackers, with the purpose of pushing IITR's security culture to new heights, mainly through conducting and taking part in CTFs. <br />
<br />
While InfoSecIITR was still in its infancy, we were still trying to figure out what might be the best way forward. However, with the experience of leading GG, I had realised that we need to strike the right balance between planning and action, in order to get optimal results. Too much planning and it is a waste of time, and it is the same for unplanned action. With this in mind, we began to come up with a rudimentary plan of action with only a small number of members (though it was an open group and anyone could join). Over time though, as 4th year rolled by, it would grow by leaps and bounds (with over 100 first yearites showing up for some meetings), and we would have come up with a much more concrete plan of what to do next. <br />
<br />
As we started taking part in more and more CTFs over the year, I realised that there were some teams, at an international level, that did consistently well. One of these is PPP -- a team from the Carnegie Mellon University, that has consistently won almost all the most difficult CTFs that happen each year. Looking into their structure (mainly to figure out how to help InfoSecIITR progress more), I found that it has a faculty advisor who does research in the same field -- software security. Wait, seriously?! You could take this hobby up as a full career? Even though I was reading papers in security before, I had suddenly found out that academia considered this a complete field! After a lot of reading of papers, thinking, and testing some ideas, I decided to apply for a summer research internship under Prof David Brumley -- the aforementioned faculty advisor. <br />
<br />
After a bunch of emails back and forth, he was happy to invite me over to CMU for a fully funded summer internship. This intern was arguably the best time I've ever had while working, probably because it didn't feel like work at all. I was helping develop systems to augment humans in finding vulnerabilities in common software. Additionally, this is where I fell in love with using Emacs (it is better than Vim, but I digress again), started loving OCaml, and figured out that this field is probably what I want to continue in for the foreseeable future.<br />
<br />
Once back in Roorkee, 4th year began, and with it, came the whole "tension" of applying for further studies. While batch-mates prepared for job interviews, I had decided that I wanted to go for a PhD. Taking up the standardised examinations, asking for letters of recommendation, writing a statement of purpose, updating my resume, filling out forms -- it does turn out to be a very time-consuming task. However, it indeed is a very rewarding task if done right, in two major ways -- it helps you really think about all you have done and what you want to do further in life, and it provides a sense of confidence in knowing that you can really achieve all that you wish to (since you've achieved a lot of what you originally set out to do, and even when goals changed, you've adapted and done well). <br />
<br />
Managing time between all these, as well as the Bachelor Thesis Project (BTP), a whole semester flew by almost instantly; all the applications to the 5 institutes I had applied to were also sent. What now?! Then began the long and dreadful wait (at least, as described by others). The last semester of college was one where compared to the previous 7 semesters, I had very little to really do. Academics had gotten very chill, BTP was going fine, campus groups were being handled easy enough, I'd gone on multiple trips/treks, I was taking part in multiple contests, and yet I had time to spare. So I decided that I would spend my free time divided amongst 2 main things -- spending much more time with those I am close to, and helping juniors out on a larger scale.<br />
<br />
Over the previous few years, I had formed extremely strong bonds with a lot of people on campus -- people I loved spending time with, whether they were juniors, seniors or batch-mates. However, each of us were busy with our own things until then. Now, with the little bit of extra free time on our hands, we could spend more quality time. Each moment spent definitely becomes more precious, as the time to go apart draws closer. <br />
<br />
Apart from this, while I had already been helping juniors out in various ways, mainly through mentoring or just being there for advice when needed, I decided that I should start working on making a larger impact on the general crowd, and help move IITR's culture more towards research. Over the years, I had tried pushing for this culture in as many ways that I could, but now it was time to reach out to as many as possible, before I bid adieu. So, along with others who had done research interns, and others who were doing research, I took a few talks, and reached out to everyone who was interested (even casually) in considering research as a career possibility. Turns out, there are many who want to try things, but just don't know whom to approach. I realised that it became a moral duty for those of us who had been through the pains of starting off, without having any guidance, to actually guide those who wanted to pursue their dreams; and this was amongst the most fulfilling things I have ever done. <br />
<br />
While all this was going on, the decision letters started to arrive from the different institutes, and I had gotten selected into 3 really amazing places -- MIT, UCSB, and CMU. And suddenly, I had a problem -- how can you really decide between 3 of the best places for the kind of research I wanted to do? Of course, getting selected into any of these is a matter of joy and pride, but getting into all 3 is a bit of a problem. Of course, it is a good kind of problem to have though. After much deliberation, I decided that I would go with CMU. And with that, began the farewells, of the different campus groups, as well as the department. <br />
<br />
It doesn't hit that hard until you reach the point of the farewells, how much you have come to love the time spent over the 4 years. It is at this time that many tend to get emotional since, for some of us, it might be a very very long time until we meet again. Thankfully though, the tradition of dressing up as different characters (such as Jack Sparrow, or Davy Jones), does provide a bit of necessary relief from the otherwise extremely emotionally charged farewell. <br />
<br />
However, even after all of this, Roorkee doesn't let you go. The final semester exams, and the final BTP evaluation happen after the farewells, and even after that comes up the extremely amazing tradition of the "no-dues". Most people really understand these pains only when they need to rush through campus, in the hot sweltering sun, just to get a few signatures on pieces of paper that are probably gonna be thrown away in almost no time. Yet there is a kind of fun in everyone cursing the same people and the tradition each year, standing in those long queues, waiting for those coloured slips of paper. <br />
<br />
Soon enough though, even that is done, and it comes time to finally say goodbye, and it really breaks my heart to say goodbye. It was an amazing 4 years, and I am going to cherish these memories forever. A lot of the connections and friendships that I have made, cannot even be put into words, but I feel that those are what I am going to remember more than anything else. I believe it is the people, and not the place, that really grows on you. <br />
<br />
If I have any advice for 1st yearites, it would be this: across the 4 years, not everything you do has visible benefit, and not everything will get to the resume. Not every part of it needs to be for a predestined goal. Nor does it need to be just smooth-going successes. Do not limit yourself to only academics, but neither let it suffer. You will stumble, and you will struggle, but that is part of the process. You just got to keep your head cool and keep moving forward, trying new things, finding new interests, building strong friendships, and enjoying your time at college. Because as long as you don't waste them, these 4 years are definitely going to become a story to tell.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-80736491124142650332016-01-13T17:49:00.000+05:302016-01-13T17:49:50.108+05:30 Writeup for n00b16CTFAh! Year 2 of n00b ctf @ <a href="https://backdoor.sdslabs.co/" target="_blank">backdoor</a>. Quite a nice and fun contest. Though this contest was for n00bs, I decided to take part again (just coz I won last time - find the writeup for those questions <a href="http://jaybosamiya.blogspot.in/2015/01/writeup-for-n00b15ctf.html" target="_blank">here</a>). This time, I came second, since I couldn't solve 2 of the questions, and one other team (dcua) solved all except 1. However, a short while after the contest was done, I solved another. Now only the question titled EULA remains. Hopefully, I'll update this post with its writeup soon too :)<br /><br />Here's a bunch of writeups (more like small hints) for each of the questions I solved:<br />
<br />
<b>Batman</b><br />
<br />
Take a look at the URL as you click on the items. Maybe higher numbered items are interesting (even if they cannot be directly accessed). The Hackbar add-on for Firefox makes this very easy to go through, btw.<br />
<br />
<b>Bin-Easy</b><br />
<br />
Okay, I didn't even run the binary. The answer was just lying there in one of the strings (hint hint) inside it directly. Pre-execution-analysis itself showed up the flag.<br />
<br />
<b>Bin-Medium</b><br />
<br />
We can disassemble this executable and change the path of execution to either circumvent the check (through gdb) or by flipping one bit in the binary. Each of these would print the flag. Another thing is to try to work out how the flag is being made in the memory, but that's just wasting your time. Take the easy path :P<br />
<br />
<b>EULA</b><br />
<br />
Still unsolved by me. However the <span style="font-family: "Courier New",Courier,monospace;">Accept-Language</span> HTTP parameter seems very interesting, especially with things like <span style="font-family: "Courier New",Courier,monospace;">en</span>, <span style="font-family: "Courier New",Courier,monospace;">it</span> etc.<br />
<br />
<b>Fool</b><br />
<br />
A very high stake challenge (it had 150 points) but it a very short while, it was obvious it is a format string bug. After that it is trivial to attack it (read up on FSBs if it isn't). I made a stupid mistake though which took a couple of minutes to realize. I was sending a single quote at the beginning and at the end. Doh!<br />
<br />
<b>Frost</b><br />
<br />
A multi byte xor cipher. My favourite tool for this (<a href="https://github.com/hellman/xortool" target="_blank">xortool.py</a>) works directly.<br />
<br />
<b>Magic</b><br />
<br />
The <span style="font-family: "Courier New",Courier,monospace;">=</span> at the end gives away that it is base64 encoded. Decoding it gives another cipher but the spacing makes it obvious that it must be some simple ancient cipher. Caesar would be proud.<br />
<br />
<b>Matrix</b><br />
<br />
I couldn't solve this challenge during the contest, but solved it just after it, and damn, was I over thinking it. During the contest, I realized that the <span style="font-family: "Courier New",Courier,monospace;">g</span>s were too regular (every 7th place) so I split it into 32 lines of 6 characters each (after removing the <span style="font-family: "Courier New",Courier,monospace;">g</span>s at the end of each line). All these were hex digits, and with the 6 character thing, I naturally thought of colours (for example, #00ff00 is green). Lot of time was wasted in this direction, but after the contest and a small hint of transposing the matrix (i.e. making it into 6 rows of 32 characters each), it was obvious that each of those could be hashes. Online MD5 crackers then gave away the answers.<br />
<br />
<b>Rbash</b><br />
<br />
Restricted bash - where <span style="font-family: "Courier New",Courier,monospace;">cd</span> wasn't allowed. Well, <span style="font-family: "Courier New",Courier,monospace;">ls -l ..</span> worked. And there was the flag right there to be <span style="font-family: "Courier New",Courier,monospace;">cat</span>ed to the screen. Later on, I found out that you could also execute <span style="font-family: "Courier New",Courier,monospace;">sh</span>ell inside this rbash and then you could do anything you wanted!<br />
<br />
<b>Robot</b><br />
<br />
The name of this challenge gave away that we needed to look at robots.txt (that pesky little file that web crawlers are supposed to adhere to, but only lead to attackers finding things they shouldn't).<br />
<br />
<b>Wahtzdis</b><br />
<br />
Whoa! That is a lot of data, but seems like the javascript console in the browser nicely handles it. Turns out this is the esoteric language <a href="http://esolangs.org/wiki/JSFuck" target="_blank">JSFuck</a>.<br />
<br />
<br />
Did you find any other cool/new ways of solving any of these tasks? If so, leave a comment below.
Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com22tag:blogger.com,1999:blog-4785709442637044434.post-17271511912852416402015-01-23T16:40:00.000+05:302015-01-23T16:42:07.066+05:30Dracula UntoldA thrilling origins story that would make for a great video game.<br />
<br />
<div class="separator" style="clear: both; text-align: center;">
</div>
<div style="clear: left; float: left; margin-bottom: 1em; margin-right: 1em;">
<img border="0" src="http://1.bp.blogspot.com/-Oz62t5803cA/VMIrYxy8HrI/AAAAAAAAAmQ/S_k0jX3BeNc/s1600/dracula-untold.jpeg" height="260" width="400" /></div>
<br />
<br />
<br />
Vlad is a Prince whose family is threatened by the Turks. In order to save his family and the people of his country, he must seek a power much greater than any human can have. But with that power comes a price much greater than a human should bear. He must struggle to keep his humanity and save his people.<br />
<br />
Personally, I loved the story, but felt that the ending was such a huge cliff-hanger, it deserves a sequel. If there were to be a sequel, it will definitely be one that surpasses Dracula Untold. With amazing acting by every member of the cast, combined with a well written origin story (though hardcore Count Dracula fans would dismiss it), topped off with good directing and visual effects, this movie is definitely one to watch.<br />
<br />
Some criticism is required however. A lot of the story line was given away in the trailer itself, so if you've seen the trailer in advance (as I did), you'll find that the movie only does some filling in of details (and the bad ass ending, which I have been going on about). This movie is not one to be seen multiple times. Also, it does feel like the movie could've been an awesome game instead. Imagine doing the bat changing thing! If a sequel were to be made however, which continued right where this one ended, I would definitely want to watch it in theaters.<br />
<br />
So, what did you think of this movie? Leave your comments below.<br />
<br />
PS: Turns out that a sequel might actually be done (executive producer Alissa Phillips revealed so).Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-5972478851278703832015-01-05T00:29:00.004+05:302016-07-14T00:51:12.817+05:30Writeup for n00b15CTFThis is a collection of hints for all the problems in the recently conducted Capture The Flag (CTF) contest conducted by SDSLabs as a way to get n00bs (beginners) to have a taste of the beautiful world of hacking. It was a pretty fun contest even though it was quite easy.<br />
<br />
<h3>
Test </h3>
<br />
Use a SHA256 tool. My favourite is to just search for "SHA256 STRING_TO_BE_SHA256" on my default search engine (www.duckduckgo.com) <br />
<br />
<h3>
Location-51 </h3>
<br />
There is a redirect occuring here from http://hack.bckdr.in/LOCATION-51/index.html to http://hack.bckdr.in/LOCATION-51/trap.html Stop this redirect, and read the source of index.html The javascript there gives away the flag <br />
<br />
<h3>
Hidden flag - Easy </h3>
<br />
Using the <span style="font-family: "courier new" , "courier" , monospace;">file</span> linux command, we find out that it is an ELF binary, but running it gives nothing. However, running <span style="font-family: "courier new" , "courier" , monospace;">strings</span> on it gives away the flag. <br />
<br />
<h3>
Search </h3>
<br />
The zip file contains a .txt file which does not seem normal text, so we run a file on it. This says that it is jpeg, so change it to .jpg and open it. It is a QR code. Decode this using some online tool (just search for "QR code decode online" for a large number of free tools) and get a link. The link has the flag. <br />
<br />
<h3>
Lost </h3>
<br />
The message says Console, so open up console in Firefox. The message then tells you to POST data to a link. Going to this link directly does nothing, but sending it any random POST data (using HackBar addon in Firefox for example) gives the flag. <br />
<br />
<h3>
Hidden flag - Medium </h3>
<br />
Analyzing the file with IDA Pro shows that there is a function called <span style="font-family: "courier new" , "courier" , monospace;">print_flags() </span>which is not called inside <span style="font-family: "courier new" , "courier" , monospace;">main()</span>. Running this function should print the flag. We can do this by attaching <span style="font-family: "courier new" , "courier" , monospace;">gdb</span> to the binary, breaking the execution and running the <span style="font-family: "courier new" , "courier" , monospace;">print_flags()</span> function. <br />
<br />
<h3>
Clutter </h3>
<br />
Extracting the file and analyzing with Wireshark shows that there is too much to work with. But exporting all the files and then running <span style="font-family: "courier new" , "courier" , monospace;">strings</span> on it would probably work. However, filtering this is a pain, so I just ran a <span style="font-family: "courier new" , "courier" , monospace;">grep</span> for flag and the answer will be visible near a pastebin title. <br />
<br />
<h3>
No - Signal </h3>
<br />
Use GIMP or Photoshop to add the images. The flag should be obvious then. <br />
<br />
<h3>
Sound </h3>
<br />
Slow down and reverse the sound wave using Audacity. Listen to it and it should be obvious what the flag is. <br />
<br />
<h3>
Sequel </h3>
<br />
Looking at the code, it seems like a SQL injection can be done here. Downloading the database.sdb file and rewriting the source code to start throwing data from database, you realize that there is no user sdslabs in the database. This makes it obvious that you need to add the user. The following username virtually that: <span style="font-family: "courier new" , "courier" , monospace;">' UNION SELECT 'sdslabs','sdslabs','sdslabs','sdslabs','0c4ea8f5b344600f78516334254e9e085f2225a42a0bb18fa8bd774589f1ca19' UNION SELECT * FROM users WHERE '0'='1</span>. Note that this query will not work directly, the password will have to be set accordingly. <br />
<br />
<h3>
Undisputed </h3>
<br />
The file is a ext4 filesystem (use <span style="font-family: "courier new" , "courier" , monospace;">file</span> command if you don't trust the extension). Mount this in linux using the <span style="font-family: "courier new" , "courier" , monospace;">mount</span> command (read <span style="font-family: "courier new" , "courier" , monospace;">man mount</span> to know how) and then open the file inside to see the flag.<br />
<br />
<br />
<br />
Did you find any other cool/new ways of solving any of these tasks? If so, leave a comment below. <br />
<br />
<a href="https://jaybosamiya.blogspot.com/2016/01/writeup-for-n00b16ctf.html" target="_blank">Link to writeup for n00b16ctf</a>Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com32tag:blogger.com,1999:blog-4785709442637044434.post-16573484612738424742014-12-14T00:37:00.000+05:302019-03-18T11:29:07.276+05:30How to Start Competitive ProgrammingIf you've ever thought about competitive coding, all you've got to do is start now. Doesn't matter which class or branch you are in. Everyone can code and everyone can be competitive. Basically, all you've got to have is the right mindset and the right skill set.<br />
<br />
Let's talk about the mindset first. Competitive programming requires a drastically different mindset when compared to "normal" (or developmental) programming. While in developmental programming you have to concentrate on writing quality code that is manageable, competitive programming generally involves writing code that "just works". This is because you'll probably never even look at your code again, once you get an AC (accepted) result from the grader. This does not mean that you should write sloppy code since that would just make it hard to debug (and this can be a real pain in the a** in a competitive setting, with the added pressure of time running out). All it means is that the code need not have extensive documentation (just some inter-spread comments to help out when debugging are enough) or modularity/objects/classes (just write it in logically separate functions to make life easier).<br />
<br />
What about the skill set? Basically, the only requirement is that you should be able to write in the language that the grader accepts without having to look at the documentation for the basics. Since almost all graders support C++ (I haven't found any that don't, except in some "special language contests" etc), and C++ has a massively powerful library called STL (standard template library), C++ is the natural choice for most competitive coders. However, if Java is your mother tongue, a fairly large number of graders accept this as well, but do note that Java is known to be slightly slower and more cumbersome to write in a pressured setting. Java does have one major advantage over C++ and this lies in its BigInteger library. However, this is so rarely used that it isn't worth the hassle of doing everything in Java just for this. Most coders use C++ for everything except for when the question requires large integers (larger than 10^18 or so).<br />
<br />
I've put together a small set of FAQs below and this should help. If you do have any more questions, do ask in the comments below.<br />
<br />
Q: Which language should I use?<br />
A: C++ (Read above for why)<br />
<br />
Q: How should I learn C++?<br />
A: The tutorials on <a href="http://cplusplus.com/" target="_blank">cplusplus.com</a> are extremely useful (<a href="http://www.cplusplus.com/doc/tutorial/" target="_blank">http://www.cplusplus.com/doc/tutorial/</a>). Not to mention, their documentation is in depth and is useful later on also, when learning things like STL.<br />
<br />
Q: Any specifics of the language that are more useful?<br />
A: C++ is a very powerful language with a gazillion features (and more added with C++11), but a whole large chunk of them are not necessary whatsoever for competitive programming. Basically, you should be comfortable with variable types, I/O (using cin, cout - there are faster ways but those are usually not necessary unless a 0.001 second improvement is the only thing that's causing a TLE - usually, the algorithm can be improved instead), control statements (if, ?: operator), looping (for and while, break and continue), functions (call by reference and call by value), arrays, strings (as character arrays), struct. Once you're comfortable with these, learn how to use basics of STL (<a href="http://www.cplusplus.com/reference/vector/vector/" target="_blank">vector</a>, <a href="http://www.cplusplus.com/reference/algorithm/sort/" target="_blank">sort()</a> are most useful). Pointers and dynamic memory is usually a larger headache than anything in the pressures of a contest. See a further question for more. Also, classes and objects will usually not be used since your code usually depends heavily on algorithms and does not usually break down into a object-oriented way.<br />
<br />
Q: What do I do for unknown sizes of memory? Is <span style="font-family: "courier new" , "courier" , monospace;">int x[n];</span> OK? Can I use pointers for this (using <span style="font-family: "courier new" , "courier" , monospace;">int *x = new int[n];</span>)?<br />
A: NO!!! <span style="font-family: "courier new" , "courier" , monospace;">int x[n];</span> is NOT OK. Arrays need to have a compile time constant size. <span style="font-family: "courier new" , "courier" , monospace;">n</span> is not a constant at compile time. Pointers and dynamic memory is too much of a headache. Just declare an array that is of the size that is max allowed (based on question). If question says n is less than 10^6, then just declare <span style="font-family: "courier new" , "courier" , monospace;">int x[1000010];</span>. The extra 10 is just to be safe :P. Oh, and put large arrays in global scope (declare outside the function) so that it doesn't cause stack overflow problems (can cause SIGSEGV on graders). And don't forget to initialize them using loops whenever necessary. If you really need a truly dynamic sized array, don't use pointers, use std::vector (<a href="http://www.cplusplus.com/reference/vector/vector/" target="_blank">http://www.cplusplus.com/reference/vector/vector/</a>).<br />
<br />
Q: Where do I learn algorithms from?<br />
A: Best place I've found is the MIT OpenCoursware. It is a BTech level course (but usually understandable by most Indian school students too). Link: <a href="http://ocw.mit.edu/courses/electrical-engineering-and-computer-science/6-006-introduction-to-algorithms-fall-2011/" target="_blank">http://ocw.mit.edu/courses/electrical-engineering-and-computer-science/6-006-introduction-to-algorithms-fall-2011/</a><br />
<br />
Q: What if I prefer books instead of videos?<br />
A: You might've heard of the book we fondly call "murder-weapon" due to it's size. CLRS (Introduction to Algorithms by Cormen, Leiserson, Rivest, Stein) is like the bible of algorithms. If you have the guts to read this huge book, by all means, please do. However, if you want something smaller and more manageable, try the book by Skiena (The Algorithm Design Manual).<br />
<br />
Q: Which sites should I practice on?<br />
A: <a href="http://www.spoj.com/" target="_blank">SPOJ</a> has the largest collection of problems. <a href="http://www.codechef.com/" target="_blank">CodeChef</a> has a very nice classification of Easy, Medium, Hard problems. <a href="http://uva.onlinejudge.org/" target="_blank">UVa</a> has a large number of problems suitable for <a href="http://en.wikipedia.org/wiki/ACM_International_Collegiate_Programming_Contest" target="_blank">ICPC</a> training. <a href="http://codeforces.com/" target="_blank">CodeForces</a> holds extremely regular contests (and editorials are also regular). TopCoder has regular SRMs but has a very messy arena applet that you have to get used to (but tutorials on TopCoder are great). <a href="https://www.hackerrank.com/" target="_blank">HackerRank</a> has a nice set of problems divided by difficulty and topic. Finally, it is up to you. I currently use UVa and CodeForces the most, but would suggest CodeChef for beginners due to its classification.<br />
<br />
Q: What to do if I get a TLE (Time Limit Exceeded)?<br />
A: Usually your algorithm might not be good enough. Check if the number of elemental operations (like single element access or write or operation etc) totally stays bounded by 10^6 or 10^7. If so, it should run within a second. Otherwise, you're in trouble. Even an algorithm that takes 10^8 operations would be too slow. For example, on an array of size 10^5, a sort using bubble sort (requiring quadratic time) is too slow, but merge sort (requiring N log N time) runs within a second.<br />
<br />
Q: What to do if I get a MLE (Memory Limit Exceeded)?<br />
A: You really need to cut down on what memory you are using. Reuse memory space if possible. Usually this verdict from a grader is very very rare. I've got it only once or twice totally in my whole experience until now, and it was fixed by rethinking the usage of memory. A million sized array if integers takes up 4 MB of space, and million 'long long's take up 8 MB space, so this is usually not a problem at all.<br />
<br />
Q: What to do if I get a WA (Wrong Answer)?<br />
A: Check if you are missing any <span style="font-family: "courier new" , "courier" , monospace;">\n</span> while outputting your answer. This is a common mistake that might happen even if code and algo is correct otherwise. If that isn't the problem, try running the algo on paper and see that it matches for all cases you can throw at it. If it still works, you haven't tried some corner cases (n=0,1, or very very large). Also, are you sure you are using the right data type? int stores max of ~10^9, long long stores ~10^18. Use it instead. Remember, intermediate calculations also should fit within the limit. If all else fails, try rethinking the algorithm.<br />
<br />
Q: I cannot figure out the algorithm. What should I do?<br />
A: If this is in a contest, there is usually not much you can do other than just think or move onto another question. However, if this is when practicing, try working out the example on paper first to make sure you've understood the question. If nothing yet, don't give up (or check online yet). Mentally take note of the question and go on with other work. The answer will strike at the most random time (in the shower for instance). If you still get nothing (after a few days/weeks/months depending on difficulty of question), search for an editorial for the question, or ask someone who's solved it. If it involves a new concept, learn it (don't just copy code without understanding). If it did not require anything new, then re learn whatever was needed. After that, try coding it in and getting an AC. Search for related concepts and questions and solve them.<br />
<br />
Q: I know the algo, but cannot code it in. What should I do?<br />
A: Isn't this obvious? Relearn the topics needed.<br />
<br />
Q: Can you see my code for problem XXX from site YYY?<br />
A: Nope. I do not have the time to do this individually. Also, competitive code is usually hard to read and difficult to find mistakes in. I usually cannot understand my own (competitive) code after a few days (developmental code is understandable even after years however, since it is written that way). You're on your own. However, if you write the algo in simple English (or pseudo code) then it might help for you to figure out what is wrong by yourself. Also online forums exist just for this. If nothing else, if you can find me a great question, I might just write an editorial on it (see example here).<br />
<br />
Q: My question is not in this FAQ.<br />
A: Write it in the comments below.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com9tag:blogger.com,1999:blog-4785709442637044434.post-78974803605776195932014-12-03T09:30:00.000+05:302014-12-03T09:30:04.195+05:301000 Week MarkTurns out, I was born exactly 1000 weeks before today. Next such round number happens in 2018 when I'd have lived for 200,000 hours on this hunk of rock that we call Earth. All this cool calculation is done very nicely using the <a href="http://www.timeanddate.com/date/birthday.html" target="_blank">Special Age Calculator</a> on the website <a href="http://timeanddate.com/">timeanddate.com</a>.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-56147355526320947282014-11-26T23:41:00.000+05:302014-11-26T23:41:53.782+05:30Debugging code in a competitive setting, Part 1<br />
Writing code in a competitive setting is an especially tiring and frustrating task, for a multitude of reasons. The rush of wanting to code fast prevents one from applying good coding standards and leads to trivial errors. Also, there is no time to set up a testing framework etc. How do you prevent (or at least find and correct) any errors in the code you write?<br />
<br />
What I personally do is to use a combination of <span style="font-family: Courier New, Courier, monospace;">gdb</span> and a custom debug message function.<br />
<br />
The first part of this series of posts will explain the function<br />
<br />
First, I always put the following code at the start of my programs:<br />
<br />
<span style="font-family: Courier New, Courier, monospace;">#ifdef DEBUGIT</span><br />
<span style="font-family: Courier New, Courier, monospace;"> #define DEBUG(X) cerr << ">>> DEBUG(" << __LINE__ << ") " << #X << " = " << X << endl</span><br />
<span style="font-family: Courier New, Courier, monospace;">#else</span><br />
<span style="font-family: Courier New, Courier, monospace;"> #define DEBUG(X) (void)0</span><br />
<span style="font-family: Courier New, Courier, monospace;">#endif</span><br />
<br />
Now, whenever there is a need to check the value of a variable (or expression), all that is left to be done is to call the <span style="font-family: Courier New, Courier, monospace;">DEBUG()</span> function like so:<br />
<br />
<span style="font-family: Courier New, Courier, monospace;">DEBUG(x); // debugging variable x</span><br />
<span style="font-family: Courier New, Courier, monospace;">DEBUG((a<<3)+2); // debugging an expression</span><br />
<br />
The way that the "function" (or macro, to be precise) is defined, whenever <span style="font-family: Courier New, Courier, monospace;">DEBUGIT</span> is defined at compilation, debug statements are shown, and otherwise, they are just skipped.<br />
<br />
Hence, whenever you want to look at the debug statements, use <span style="font-family: Courier New, Courier, monospace;">g++ -DDEBUGIT</span> to compile instead of just <span style="font-family: Courier New, Courier, monospace;">g++</span>.<br />
<br />
Here's an example program and its output:<br />
<br />
<span style="font-family: Courier New, Courier, monospace;">#include <iostream></span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: Courier New, Courier, monospace;">using namespace std;</span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: Courier New, Courier, monospace;">#ifdef DEBUGIT</span><br />
<span style="font-family: Courier New, Courier, monospace;"> #define DEBUG(X) cerr << ">>> DEBUG(" << __LINE__ << ") " << #X << " = " << X << endl</span><br />
<span style="font-family: Courier New, Courier, monospace;">#else</span><br />
<span style="font-family: Courier New, Courier, monospace;"> #define DEBUG(X) (void)0</span><br />
<span style="font-family: Courier New, Courier, monospace;">#endif</span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: Courier New, Courier, monospace;">int main() {</span><br />
<span style="font-family: Courier New, Courier, monospace;"> int x = 5, y = 10;</span><br />
<span style="font-family: Courier New, Courier, monospace;"> DEBUG(x);</span><br />
<span style="font-family: Courier New, Courier, monospace;"> DEBUG(y);</span><br />
<span style="font-family: Courier New, Courier, monospace;"> ++x += y++;</span><br />
<span style="font-family: Courier New, Courier, monospace;"> DEBUG(y+1);</span><br />
<span style="font-family: Courier New, Courier, monospace;"> cout << x << endl;</span><br />
<span style="font-family: Courier New, Courier, monospace;">}</span><br />
<br />
Output:<br />
<br />
<span style="font-family: Courier New, Courier, monospace;">>>> DEBUG(13) x = 5</span><br />
<span style="font-family: Courier New, Courier, monospace;">>>> DEBUG(14) y = 10</span><br />
<span style="font-family: Courier New, Courier, monospace;">>>> DEBUG(16) y+1 = 12</span><br />
<span style="font-family: Courier New, Courier, monospace;">16</span><br />
<br />
The advantage with the DEBUGIT technique is that you can directly submit code (without any modifications) and the grader will not run the DEBUG statements at all.<br />
<br />
I have added the following line to my .bashrc file:<br />
<br />
<span style="font-family: Courier New, Courier, monospace;">alias d++='g++ -DDEBUGIT'</span><br />
<br />
Hence, I can directly run d++ for compiling with the debug statements.<br />
<br />
In my next post, I will explain how to use <span style="font-family: Courier New, Courier, monospace;">gdb</span> to further make life easier.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com2tag:blogger.com,1999:blog-4785709442637044434.post-40621623290123447372014-11-24T13:52:00.000+05:302014-11-24T13:53:36.870+05:30Terminal based Spell CheckHere's a cool little script I wrote (added to my .bashrc) file in order to test spellings, or to generate them when I don't remember them.<br />
<br />
<pre>function spelling {
if [ $((`grep -c "^$1$" /usr/share/dict/american-english`)) -gt 0 ]; then
echo -e "Spelling of\e[1;32m" `grep -m 1 "^$1$" \
/usr/share/dict/american-english` "\e[0mseems fine"
else
echo -e "\e[1;31mThere seems to be a mistake in spelling\e[0m"
fi
}
</pre>
<br />
The script is run quite simply by saying "spelling word-to-be-checked". For example,<br />
<pre>spelling look</pre>
would say<br />
<pre>Spelling of <span style="color: lime;">look</span> seems fine</pre>
but<br />
<pre>spelling louk</pre>
would say<br />
<pre><span style="color: red;">There seems to be a mistake in spelling</span></pre>
<br />
Where this is extremely useful is when you cannot remember some part of the spelling of a word. For example allitaration or alliteration. Here, I can just use a regex.<br />
<br />
Running<br />
<pre>spelling allit.ration</pre>
would say<br />
<pre>Spelling of <span style="color: lime;">alliteration</span> seems fine</pre>
thereby giving the right spelling.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-53253307981561646602014-10-29T22:33:00.000+05:302014-10-29T22:54:30.609+05:30Editorial for Blitzkreig "Lost Zucky"A nice problem based on choosing a proper method to denote state and then implementing it correctly and efficiently.<br />
<br />
Let's first look at the question:<br />
<br />
<pre><span style="font-size: x-small;"> Problem Statement:
Zucky wants to find his way out of a maze in minimum possible steps.
Zucky knows that he can get lost in the maze if he can't find the exit so
he decides to find a way by writing the code first. Now, he knows that
there are doors, keys and walls in the maze. Doors and keys can be of four
colors Red, Blue, Green, Yellow (RBGY) and red, blue, green, yellow (rbgy)
respectively. (Capital letters represent doors, lower case letters
represent keys). Every key can open the door of same color as its own. For
eg. r can open R, g can open G, etc. No one can get through the walls.
Now, being a busy person he can't write all the code. So, he turns to you
for help. Your task is to find minimum number of steps in which he can get
out of the maze.
Note: Zucky can move only in horizontal and vertical direction.
Input:
The first line contains t, the number of test cases (1 ≤ t ≤ 5).
The second line contanis two integers R, C (1 ≤ R, C ≤ 100)
Then R lines follow. Every line contains C characters, which can be
1) R, B, G, Y - doors,
2) r, b, g, y - keys,
3) # - wall,
4) . - free space,
5) * - start point,
6) X - exit
Output:
Each line should contain number of steps required if a path exists and
"Trapped!" if there is no path.
Example:
Input:
2
1 10
*...rRG..X
2 5
*gr##
RG..X
Output:
Trapped!
5
Please note that there can be multiple exits, multiple keys/doors of the
same color, multiple walls, but only one start point. A key once collected
can be used to open as many number of doors.
</span></pre>
<span style="font-size: x-small;"><br /></span>
<br />
Okay, now, how do we go about solving this?<br />
<br />
Firstly, we notice that if we get rid of the RGBYrgby stuff, then all we have is a simple maze to solve (use a <a href="https://en.wikipedia.org/wiki/Breadth-first_search" target="_blank">BFS</a> on the <a href="https://en.wikipedia.org/wiki/Implicit_graph" target="_blank">implicit graph</a>).<br />
However, one can then notice that the coloured keys create nothing new, other than to multiply a factor of 2^4=16 to the number of states (i.e. for each key, whether it is picked up or not also needs to be added to the state). Noticing this, we have a very clear idea of how to implement a BFS on the implicit graph that is formed here. Each node in the graph is a state which contains row number, column number, and which keys have been picked up. <br />
<br />
Putting all of this in a <span style="font-family: "Courier New",Courier,monospace;">pair<pair<int,int>,pair<pair<bool,bool>,pair<bool,bool>>></span> might be fun to some, but to me, that's just taking it too far.<br />
What I did instead is made a struct that stores the values and wrote hash, unhash functions in order to convert this struct to and from a long long. This makes it easier to use with STL map which I used to store which vertices were already visited.<br />
<br />
Here's the state struct and hash,unhash functions:<br />
<br />
<pre> typedef long long ll;
struct state {
int row, col, r,g,b,y;
};
const ll MULT_BASE = 101;
ll hash(const state &s) {
ll ret = 0;
ret *= MULT_BASE; ret += s.row;
ret *= MULT_BASE; ret += s.col;
ret *= MULT_BASE; ret += s.r;
ret *= MULT_BASE; ret += s.g;
ret *= MULT_BASE; ret += s.b;
ret *= MULT_BASE; ret += s.y;
return ret;
}
state unhash(ll h) {
state ret;
ret.y = h % MULT_BASE; h /= MULT_BASE;
ret.b = h % MULT_BASE; h /= MULT_BASE;
ret.g = h % MULT_BASE; h /= MULT_BASE;
ret.r = h % MULT_BASE; h /= MULT_BASE;
ret.col = h % MULT_BASE; h /= MULT_BASE;
ret.row = h % MULT_BASE; h /= MULT_BASE;
return ret;
}
</pre>
<br />
<br />
The maze itself is quite simply stored in a character array:<br />
<br />
<pre> char maze[101][101];
int R, C;
</pre>
<br />
Now, we have to figure out which states are accessible from where. Also, we want to update the new state if we end up picking up a key.<br />
<br />
<pre> bool should_move(const state &o, state &n) {
if ( n.row < 0 || n.row >= R || n.col < 0 || n.col >= C )
return false;
char l = maze[n.row][n.col];
if ( l == '.' || l == '*' || l == 'X' )
return true;
if ( l == '#' )
return false;
if ( l == 'r' )
return (n.r=1,true);
if ( l == 'g' )
return (n.g=1,true);
if ( l == 'b' )
return (n.b=1,true);
if ( l == 'y' )
return (n.y=1,true);
if ( l == 'R' )
return (n.r>0);
if ( l == 'G' )
return (n.g>0);
if ( l == 'B' )
return (n.b>0);
if ( l == 'Y' )
return (n.y>0);
}
</pre>
<br />
<br />
Notice the code for picking up the keys. The syntax <span style="font-family: "Courier New",Courier,monospace;">return (n.y=1,true);</span> uses a very nice but underused feature of C/C++. The comma operator, used in an expression, executes the left side part, followed by the right side part and keeps the right side part for further evaluation. This basically makes the code do <span style="font-family: "Courier New",Courier,monospace;">n.y=1; return true;</span> but the code is much more cleaner using this comma notation since unnecessary curly braces are removed and also, the code has a smooth uniform look of returns based on conditions.<br />
<br />
Now, we can just do a BFS starting from the first location. We exit out of the BFS the moment we find any exit; thus guaranteeing shortest path.<br />
<br />
The BFS is implemented quite simply as follows:<br />
<br />
<pre> int bfs(int startrow, int startcol) {
// returns -1 if not possible to exit </pre>
<pre> map<ll,int> dist;
int ans = -1;
state startstate;</pre>
<pre> startstate.row = startrow; startstate.col = startcol;
startstate.r = 0; startstate.g = 0;</pre>
<pre> startstate.b = 0; startstate.y = 0;
queue<pair<ll,int> > q;
q.push(make_pair(hash(startstate),0));
while (!q.empty()){
ll curhash = q.front().first;
state curstate = unhash(curhash), newstate;
int curdist = q.front().second;
q.pop();
if ( dist.count(curhash) != 0 )
continue;
dist[curhash] = curdist;
if ( maze[curstate.row][curstate.col] == 'X' ) {
ans = curdist;
break;
}
newstate = curstate; newstate.row += 1;
if ( should_move(curstate,newstate) )
q.push(make_pair(hash(newstate),curdist+1));
newstate = curstate; newstate.row -= 1;
if ( should_move(curstate,newstate) )
q.push(make_pair(hash(newstate),curdist+1));
newstate = curstate; newstate.col += 1;
if ( should_move(curstate,newstate) )
q.push(make_pair(hash(newstate),curdist+1));
newstate = curstate; newstate.col -= 1;
if ( should_move(curstate,newstate) )
q.push(make_pair(hash(newstate),curdist+1));
}
return ans; </pre>
<pre> }
</pre>
<br />
<br />
Let's take a look at what's happening in this (pretty long) code. We are keeping a list of distances to visited states in the <span style="font-family: "Courier New",Courier,monospace;">dist</span> map. As is done in a normal BFS, we push the first vertex into a queue and then start a loop. However, in this case, the distances matter, and so we put an integer tagged along with the state too which will store the distance (distance means number of steps needed to reach that state). As long as the queue is not empty, we keep taking off the front element and we put all its neighbours into the queue whenever the neighbours are accessible. As soon as we reach a final destination (exit) however, we break out of the loop and return out of the function.<br />
<br />
All that remains now is to implement the necessary I/O routines and to call the right functions; and there it is - AC!!!<br />
<br />
Any doubts/suggestions/criticisms? Please leave your comments below.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-74308982827314342442014-10-22T00:58:00.001+05:302014-10-22T01:02:06.027+05:30The Easiest Way Ever to Compare 2 TextsHere's another reason to use Linux: You can use the beautiful terminal tool called <span style="font-family: "Courier New",Courier,monospace;">wdiff</span> (more useful when only certain words in a sentence may have changed, as opposed to whole sentences or code, in which case, <span style="font-family: "Courier New",Courier,monospace;">diff</span> is a better tool)<br />
<br />
How do you use it? First, you'll have to install it (simple standard "<br />
<span style="font-family: "Courier New",Courier,monospace;">sudo apt-get install wdiff</span>" is enough - HA! Let's see Windows install anything that easily!)<br />
<br />
Then, just use this crazy <i>little</i> command whenever you need to compare two documents:<br />
<br />
<span style="font-family: "Courier New",Courier,monospace;">echo "Enter text1 (press Enter,Ctrl+D when done):"; cat > /tmp/1.txt; echo "Enter text2 (press Enter,Ctrl+D when done):"; cat > /tmp/2.txt; echo "Comparing..."; wdiff -n -w $'\033[1;31m' -x $'\033[0m' -y $'\033[1;32m' -z $'\033[0m' -s /tmp/1.txt /tmp/2.txt; rm /tmp/1.txt; rm /tmp/2.txt</span>
<br />
<br />
Or, let's just make our lives easier and put all of that into a function (therefore, making it more nicely written and easier to understand too)<br />
<br />
<span style="font-family: "Courier New",Courier,monospace;">function 2compare {</span><br />
<span style="font-family: "Courier New",Courier,monospace;"> echo
"Enter text1 (press Enter,Ctrl+D when done):"</span><br />
<span style="font-family: "Courier New",Courier,monospace;"> cat > /tmp/1.txt</span><br />
<span style="font-family: "Courier New",Courier,monospace;"> echo "Enter text2 (press Enter,Ctrl+D when done):"</span><br />
<span style="font-family: "Courier New",Courier,monospace;"> cat > /tmp/2.txt</span><br />
<span style="font-family: "Courier New",Courier,monospace;"> echo "Comparing..."</span><br />
<span style="font-family: "Courier New",Courier,monospace;"> wdiff -n -w $'\033[1;31m' -x $'\033[0m' -y
$'\033[1;32m' -z $'\033[0m' -s /tmp/1.txt /tmp/2.txt</span><br />
<span style="font-family: "Courier New",Courier,monospace;"> rm /tmp/1.txt</span><br />
<span style="font-family: "Courier New",Courier,monospace;"> rm
/tmp/2.txt</span><br />
<span style="font-family: "Courier New",Courier,monospace;">}</span><br />
Now, all you have to do is call <span style="font-family: "Courier New",Courier,monospace;">2compare</span> and you will be able to compare texts.<br />
<br />
Well, let's break it down, shall we?<br />
<br />
The <span style="font-family: "Courier New",Courier,monospace;">echo</span> parts just show useful messages on the screen.<br />
The <span style="font-family: "Courier New",Courier,monospace;">cat</span> parts store the data taken as input into temporary locations <span style="font-family: "Courier New",Courier,monospace;">/tmp/1.txt</span> and <span style="font-family: "Courier New",Courier,monospace;">/tmp/2.txt</span><br />
The <span style="font-family: "Courier New",Courier,monospace;">wdiff</span> part is the scariest bit but is quite simple (as we shall see):<br />
<ul>
<li><span style="font-family: "Courier New",Courier,monospace;">-n</span> is a short way of saying <span style="font-family: "Courier New",Courier,monospace;">--avoid-wraps</span> which means "do not extend fields through newlines"</li>
<li><span style="font-family: "Courier New",Courier,monospace;">-w $'\033[1;31m' -x $'\033[0m' -y $'\033[1;32m' -z $'\033[0m'</span> sets up colours to show the differences in a much more easy to see way. <span style="font-family: "Courier New",Courier,monospace;">wdiff</span> by default shows colourless output (and shows differences using brackets etc.)</li>
<li><span style="font-family: "Courier New",Courier,monospace;">-s</span> or <span style="font-family: "Courier New",Courier,monospace;">--statistics</span> causes <span style="font-family: "Courier New",Courier,monospace;">wdiff</span> to show how many words were added, deleted etc.</li>
<li><span style="font-family: "Courier New",Courier,monospace;">/tmp/1.txt /tmp/2.txt</span> just specifies the files to be compared</li>
</ul>
The <span style="font-family: "Courier New",Courier,monospace;">rm</span> parts remove the temporary files<br />
<br />
But what if you don't want to keep rewriting that crazy long function each time you restart your terminal?<br />
You can place it at the end of <span style="font-family: "Courier New",Courier,monospace;">~/.bashrc</span> and then you'll be able to use <span style="font-family: "Courier New",Courier,monospace;">2compare</span> directly from your terminal next time onwards.<br />
<br />
This command is staying in my <span style="font-family: "Courier New",Courier,monospace;">~/.bashrc</span> probably permanently from now on. Maybe I'll post some other useful stuff I have in there in later blog posts.<br />
<br />
Do you know of any other ways of comparing files? Any new terminal tricks?<br />
Leave your comments below.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-31334528928745633562014-10-02T19:36:00.000+05:302014-10-02T19:36:00.422+05:30Going BackwardsAll the time, we are told to only keep going forwards - keep looking towards the bright future and to strive to achieve greater goals. How many times are we told that we sometimes need to move backwards?<br />
<br />
Think about a scenario where you have to jump from one building to another - you'll never jump directly from the parapet; you'll definitely move a few steps backwards to be able to take a run up in order to make a successful long jump. This applies to real life as well (in a metaphorical sense, of course). Many a times, we really need to move backwards to reassess and rethink whatever we are doing in order to be able to do a whole lot better than before. These are times when we need to backtrack whatever we've been doing or working on and start afresh.<br />
<br />
Backtracking is hard since it goes against the whole fiber of who we have been molded into by society itself. It is difficult to let go of whatever you've worked on for a helluva long time but sometimes, its just better to take a few steps back in order to be able to get a better run up and a better jump and just maybe reach a much greater goal and <a href="http://jaybosamiya.blogspot.com/2014/04/dreams-connection-to-different-time.html" target="_blank">dream</a> bigger.<br />
<br />
What do you think about this metaphor? Leave your comments below.Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com2tag:blogger.com,1999:blog-4785709442637044434.post-36620130588566290812014-10-01T18:04:00.000+05:302014-10-01T18:04:00.359+05:30NegabinaryThought you knew all there is to know about number systems? Well, here's something new to that list - Negabinary numbers. These are numbers that are written to the base -2 (negative two). What's so great about these numbers? There is no need to put any + or - to denote whether it is a positive number or not. Let's check these numbers out.<br />
<br />
The normal way a number is defined, works here as well. There are "b" number of digits in a number system of base "b". Here, we just have to change the definition to: there are "|b|" number of digits in a number system of base "b". The definition works perfectly after that. Then, we can just use the following equation:<br />
<div class="separator" style="clear: both; text-align: center;">
<a href="http://4.bp.blogspot.com/-ewV__8_6t3M/VCqfEE4913I/AAAAAAAAAiY/WHZWoN0rDFE/s1600/CodeCogsEqn.gif" imageanchor="1" style="margin-left: 1em; margin-right: 1em;"><img border="0" src="http://4.bp.blogspot.com/-ewV__8_6t3M/VCqfEE4913I/AAAAAAAAAiY/WHZWoN0rDFE/s1600/CodeCogsEqn.gif" /></a></div>
<br />
Using this we can thus generate the first few numbers (0, 1, 2, 3, 4, 5...) in negabinary: 0, 1, 110, 111, 100, 101...<a href="http://oeis.org/A039724" target="_blank"> (Sequence A039724 on Online Encyclopedia of Integer Sequences (OEIS)</a>) where 0 and 1 have usual face values.<br />
<br />
How do we convert a number to this base then? Write the number down in binary first. Then, going from right to left, at every odd place (i.e. x<sub>1</sub>, x<sub>3</sub>, x<sub>5</sub> ...), if the bit is one, propagate a carry to the next bit. Also, while moving from right to left, add all the carries.<br />
<br />
For example:<br />
<br />
To convert 15 to negabinary:<br />
<ol>
<li>Convert 15 to binary</li>
<ul>
<li>15<sub>decimal</sub>=1111<sub>binary</sub></li>
</ul>
<li>Propagate from right to left</li>
<ul>
<li>111<b>1</b></li>
<li>11<b>1</b>1</li>
<li>1<b>2</b>11</li>
<li>2<b>0</b>11</li>
<li><b>2</b>011 </li>
<li>1<b>0</b>011</li>
<li><b>1</b>0011</li>
<li>10011<sub>negabinary</sub></li>
</ul>
<li>Done! (This is correct since 16-0+0-2+1 = 15)</li>
</ol>
Conversion to decimal (or any other base) just uses the original formula.<br />
<br />
Addition is kinda done the way conversion is done, except that carries are propagated (one bit extra to the left, since 2<sub>negabinary</sub> = 110). <br />
<br />
We can similarly define the other operations as well.<br />
<br />
Let's take this onto another level itself: how about a number system that takes care of complex numbers as well (as digit strings)? I leave that upto you to figure out and comment about.<br />
<ol>
<ul>
</ul>
<ul>
</ul>
</ol>
Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-89504245811922245502014-09-28T22:14:00.000+05:302014-09-28T22:14:00.548+05:30Reaching the network's speed limit for file transferAre you tired of transferring files from one computer to another using pen-drives and their abysmally slow speeds? Ever long for something faster? Here's a nice way to transfer files insanely fast - as fast as the network would allow (Note: This is another cool reason to switch to Linux)<br />
<br />
Here's what you do:<br />
<br />
Let's say you want to send a folder called ABC from computer X to computer Y. Then, fire up terminal on computer Y first and type the following commands:<br />
<pre>hostname -I
nc -l 9898 | tar xv</pre>
<br />
"<a href="http://www.unix.com/man-page/linux/1/hostname" target="_blank">hostname</a> -I" shows all IP addresses associated with the host Y. You'll need to note these down to be used on computer X. "<a href="http://www.unix.com/man-page/linux/1/nc/" target="_blank">nc</a>" is a utility that allows for arbitrary TCP and UDP connections and listens. "-l 9898" is a flag for nc to open port 9898 and listen for connections. The "|" pipes the output of nc (i.e. whatever comes from the network) into the next command "<a href="http://www.unix.com/man-page/Linux/1/tar/" target="_blank">tar</a>" which is an archival utility. The "xv" part stands for e<b>x</b>tract <b>v</b>erbose which means that the archive coming from nc is extracted and each file name is printed out as it is extracted.<br />
<br />
Once you're done running the above command on Y, run the following command on X:<br />
<pre>tar c ABC | nc IP 9898</pre>
<br />
The "tar c" part stands for "use tar to compress" ABC (the folder to be sent). IP is the IP address got from the "hostname -I" command on computer Y. "nc IP 9898" connects to computer Y on port 9898 and sends the data from the tar command to the other computer.<br />
<br />
Since no extra data is transferred in this way, the data should be transferred at the maximum (theoretical) limit of your network. If your network is unstable, this might actually cause a problem since no error correction codes are sent; however, if your network is stable (or all you are sending is movies or the like) then it shouldn't matter much.<br />
<br />
Do you know of any other fast ways to transfer data on the network? Leave a comment below. :)Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-40845877271117593972014-09-26T20:19:00.000+05:302014-09-26T20:19:03.166+05:30ShellshockA newly discovered bug seems to be taking the whole security and hacker communities into uproar. A huge number of posts and talks are going on in many channels. For those who haven't heard about it, it is the bash bug which affects basically almost all systems that the world depends on.<br />
<br />
What is the bash bug? To answer that, first you need to know what bash is.<br />
<br />
"bash" stands for "Bourne-Again SHell" and is the most common type of shell on any linux or mac or unix related system. This basically includes almost all servers, and can go on all the way to smart lighting (those crazy lightbulbs whose colour can be controlled by your smart phone). If you've ever seen anyone use a black screen with white text on it, chances are you've seen either the Windows Command Prompt or a shell. A shell basically allows you to type commands to execute programs on a computer.<br />
<br />
The bash bug is basically a bug that has been found in this very commonly used shell. The bug was discovered by Stéphane Chazelas, a French IT manager working for a software maker in Scotland, and was first disclosed on 24th September 2014. It basically allows for arbitrary code execution. Turns out that this bug has existed since the very first version of bash (25 years ago!!!). The bug has been nicknamed "Shellshock" and is regarded to be severe since CGI scripts using bash can be vulnerable. It is caused due to <br />
<br />
However, this is where the open source community comes into play. Within a very short time frame, a patch has been released already and many systems are no longer vulnerable to this bug. As of now, my system is no longer vulnerable only because I continuously keep updating my PC. <br />
<br />
How to test if you're vulnerable?<br />
Just run the following code in your terminal:<br />
<pre>
env x='() { :;}; echo vulnerable' bash -c "echo this is a test"
</pre>
<br />
If your system is vulnerable, it'll tell you vulnerable, otherwise it will show an error message.<br />
<br />
If you want to know more, visit the Wikipedia page on the bug at <a href="https://en.wikipedia.org/wiki/Shellshock_%28software_bug%29" target="_blank">Shellshock</a><br />
<br />
Just to mention this here: This is the only severe bug I've personally seen on linux that has such a massive impact, and even then, it got fixed almost instantly. I love the way the open source community works so quickly. :)Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-7136367091397669192014-04-06T10:30:00.000+05:302014-10-02T15:43:59.582+05:30Dreams - A connection to a different timeDr. A. P. J. Abdul Kalam once said "You have to dream before your dreams can come true." This started to make me think, what if it is not just applicable to thinking big and achieving what you want? What if just normal dreams too work this way? Think about it, has it not happened that you are in some place and you just realize that it all had happened in a dream before? Kind of like déjà vu but not quite the same.<br />
<br />
Déjà vu, is the experience of thinking that a new situation has occurred before. I am not talking about this but am talking about the phenomenon where we know we’ve been through the same situation in a dream.<br />
<br />
It is common to dream about the past and relive some of the emotional moments that we’ve had until now, but is there any sense in thinking about dreaming about the future? Do we really dream about what will happen in a day or week or year and does it really happen?<br />
<br />
We all know that when we’re in a dream, we do not really know that we’re in that dream. It is thus quite possible that we’re thinking that we’ve already been in a place in a dream when we’re in a dream. But all this becomes too much like inception (the movie, of course). Let’s just stay away from the dream inside a dream inside a dream thing.<br />
<br />
If we look at what is happening objectively, there are plenty of reasons why we may come across this phenomenon. One possible explanation is that we may just be thinking that we’ve been there in a dream whilst never having such a dream ever before. This is quite possible since our brains are quite unreliable in terms of memories, especially when it comes to dreams. It is quite well known that we cannot remember clearly what we dreamt about even just after waking up. We may just remember pieces of it and this too is fast fading. Is it not possible then, that the mind, when in some situations, can trigger partial recall and patch up pieces from different unrelated dreams into a dream coherent with the current reality?<br />
<br />
This’d then mean that the phenomenon would just be a post hoc thing that the brain does and that predicting the future is not really possible.<br />
<br />
However, consider the following scenario. You are late for work, and you know the boss is going to scream at you. It is no surprise then that s/he screams at you for being late. Your mind “predicted” the future. Is it not possible that the mind, in dreams, is doing something similar? It is known that the mind has quite a high amount of activity even when we sleep and this increases significantly during dreams. We can say that when awake, our conscious mind is in power, but when dreaming, it’s the unconscious.<br />
<br />
The unconscious mind may, in fact, have the ability to think rationally when the conscious mind cannot. It thus may be able to piece together clues that the conscious mind may be ignorant of or may be ignoring and might be able to construct possible case scenarios. Showing the scenarios in dreams may be a way of the brain letting us prepare for what’s about to come. When we realize that a certain situation occurred in a dream, we may even realize what we did in the dream and be able to take the same course of action, if it was helpful, or take a different action if otherwise.<br />
<br />
A third possibility exists, however. That the “real world” is affected in a much more powerful way by dreams. A dream may have the capacity to affect real world decisions to such an extent that we may not really have any free will. We may be forced to take decisions that’ll eventually lead us to fulfilling those dreams. A scary thought to those who have nightmares! Lazy people, however, would like this scenario since it’d mean that they’d just have to dream big to achieve big.<br />
<br />
We may never know the true nature of dreams and whether they present windows to the future or affect it. However, we know that dreams present windows to another world that is sometimes filled with possibilities that may not be possible in reality. <br />
<br />
Dreams are and continue to remain a fascinating, captivating, mesmerising and enchanting way to see the countless possibilities that exist in our universe and any others beyond. They continue to be a source of endless debates and a source of creative ideas for both art and the sciences. Just ask Kekulé who figured out that benzene must have a cyclic ring structure by dreaming of a snake biting its own tail!Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-81604880979140299452014-04-06T09:05:00.000+05:302014-10-02T15:44:27.123+05:30The Square Root of Three by Dave FeinbergI fear that I will always be<br />
A lonely number like root three<br />
<br />
A three is all that's good and right<br />
Why must my three keep out of sight<br />
Beneath a vicious square-root sign?<br />
I wish instead I were a nine<br />
<br />
For nine could thwart this evil trick<br />
With just some quick arithmetic<br />
<br />
I know I'll never see the sun<br />
As one point seven three two one<br />
<br />
Such is my reality<br />
A sad irrationality<br />
<br />
When, hark, just what is this I see?<br />
Another square root of a three<br />
<br />
Has quietly come waltzing by<br />
Together now we multiply<br />
To form a number we prefer<br />
Rejoicing as an integer<br />
<br />
We break free from our mortal bonds<br />
And with a wave of magic wands<br />
<br />
Our square-root signs become unglued<br />
And love for me has been renewed<br />
<br />
-- Dave FeinbergJay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-5074401856242623782014-01-27T21:24:00.000+05:302014-09-26T20:24:29.051+05:30Good vs. Bad<div class="MsoNormal">
Whenever we do a good deed, we feel a sense of
accomplishment or happiness. In the pursuit of chasing happiness, we try to
maximise the number of good deeds we do and minimize the number of bad deeds.
Not only religion, but the personal sense of satisfaction of doing a good thing
is what drives most to do good things. But is this just an illusion? A façade?
Many find pleasure in doing things that would be considered “wrong” by a common
person. What makes psychopaths, murderers, rapists and general criminals do
what they do? In which way are they different?<o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
There seems to be a general belief that these kinds of
people have their brains probably “wired wrong”. But then, why is it this way?
Many theories suggest that the notion of good and bad/evil stems from beliefs
and values that get ingrained and learnt since childhood or even infancy. A
child learns from his/her parents that hurting someone else or breaking things
is bad. As the child grows up, society (in the form of teachers and elders) teach
the child that one needs to do “good things”. In a religious family, the
concept of “heaven and hell” or something similar to that. <o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
Over time, the child develops a very strong sense of right
and wrong and this becomes so ingrained into the sub consciousness of the child
that the brain starts to release the pleasure/happiness chemicals whenever
doing something “good”.<o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
However, what if the society/parents did not teach the child
what is good or bad? Or what if the child had a traumatic experience that shocked
the brain into perceiving the world different from normal? Turns out, a
majority of psychopaths, murderers etc. seem to have undergone at least one
such experience in their early childhood. Some of them are orphans, had abusive
parents, or had a neighbourhood in which many “wrong” things were considered
normal, such as selling drugs, carrying firearms etc. <o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
Living in such a world, the child quickly tends to form a
very protective shell around oneself and the only things considered “good” are
ones which are to the direct benefit to the child or lead to its survival. No
wonder, their consciences with respect to harming others are unaffected by
doing anything.<o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
This makes one wonder, do we feel emotions only because we
have been told since infancy that we should? Is it actually a forced feature of
the human mind?<o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
Dexter, from the TV Series named after him, cannot feel
emotions unless he kills. By the code of Harry, he only kills criminals who
have escaped the justice system. The reason for this is because of an extremely
traumatic incident that occurred even before he could remember anything. Acting
like he can feel emotions is the only way he can survive in this world. <o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<br />
<div class="MsoNormal">
But what if all of us are only acting out emotions? What if
none of us really feel anything but “feel” emotions only as a result of our
subconscious remembering what is good or bad? These remain questions to be
pondered about for a long time.<o:p></o:p></div>
Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0tag:blogger.com,1999:blog-4785709442637044434.post-89663397400002127852014-01-26T16:06:00.000+05:302014-09-26T20:24:40.564+05:30Life after Death<div dir="ltr" style="text-align: left;" trbidi="on">
<div class="MsoNormal">
Till recent times, scientists have believed that there is no
way to know what happens after death, and that after-life, even if it exists,
could not be proven. In the recent past however, there has been an increase in
the number of ways in which people have started to think about this pretty
common question, “What happens once we die?”</div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
Most religion profess of some form or the other of “heaven”
and “hell”, and many religions profess of rebirth. While not much can be said,
scientifically, of the heaven and hell theory, many scientists now believe that
rebirth may not be a farfetched idea. In a universe which is truly infinite,
anything that can happen, must happen at some point of time or another. If we
assume consciousness to be a manifestation of the physical arrangement of atoms
and molecules, then at some other point of time (maybe in the very distant
future or past), the atoms of your body which have split apart after your
death, come together in a very similar form leading to you becoming conscious
again. Since in the time that you’re “dead”, you have no notion of time, when
you’d just die and wake up in a similar world (which could be different in a
very important aspect such as whether dinosaurs are still living or as
negligible as what you had for breakfast in the morning). <o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
A similar theory, however, assumes that the universe may as
well be finite, but that any “choice” or “decision” taken (even in the quantum
physical sense of the word) may lead to a split of the universe into a parallel
one. Hence, if you die in “this” universe, you’d be alive in an infinite number
of other universes. Since we only are conscious when we are alive, we never
will experience death. We tend to continue in whichever universe we live in.
(Though this’d mean that we’d never lose in Russian roulette)<o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
Sci-fi fans, however, propose that life is merely a
simulation being done by a more technologically advanced civilization. That
civilization too may itself be virtual, hence, we may actually be a simulation
in a simulation in a simulation (and so on). This was formalized and brought to
the attention of the scientific community by Nick Bostrom in 2003, with a paper
titled 'Are You Living in a Computer Simulation?'</div>
<div class="MsoNormal">
<o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
Atheists, on the other hand, believe in the theory of “nothingness”
which says that consciousness passes back into the oblivion that existed before
birth.<o:p></o:p></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
Personally, I like the persistent illusion theory that
Einstein supported. It says that linearity of time is but a mere persistent illusion;
that past, present and future are merely states of the mind. If a person died
before me in this world, it’s only my illusion of time that tells me this.
Reality may be very different. <o:p></o:p></div>
<br />
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
Which one of these theories are true? We probably will never
know, but we may even probably never need to know. With advances in science and
medicine, it may be possible to stop or even reverse aging. Fatal wounds or
infections could be remedied instantly. In such a world, “death” may just
become folklore or a myth. Will this happen in our lifetime? And what kind of
consequences will this have? We do not know yet, but the answers to these sure
will lead to many interesting new breakthroughs.<o:p></o:p></div>
</div>
Jay Hitesh Bosamiyahttp://www.blogger.com/profile/15460410537396778863noreply@blogger.com0