Testing OAuth2 (Refresh Tokens) Locally

Recently, I have been trying to develop a tool that involves the use of OAuth2 and here I try to explain the steps I have taken to make it work locally on my laptop. I am particularly interested in obtaining refresh tokens so I would follow the path related to it..

I employ Authlib for the OAuth2 server and follow its documentation to build the client. The OAuth2 server documentation is here and the client documentation is here¹. Since we are interested in getting refresh tokens, we need to follow the Authorization_Code flow of OAuth2 (see here). Now, we get into the details. First of all, since we want to test the OAuth2 server locally and Authlib requires HTTPS connection to Token server², we need to make sure that the client (make it browser, Python code or curl) to the Token server has the relevant certificates and trusts in place for the local machine. I will first create a self-signed certificate for my machine (localhost) and add it to relevant certificate store. I am testing everything in Python so I will go through that path for the store as the requests module of Python uses its own certificates instead of the operating system level certificates. So if you have the certificates already installed to the operating system for the localhost (127.0.0.1) that may not work. I followed this quick list of openssl commands to generate CSR (Certificate Signing Request) and a signed X509 certificate with my own key, as follows:

- Create a Certificate request:
openssl req -out CSR.csr -key ~/.ssh/id_rsa -new

- Create a certificate with the given key and CSR:
openssl x509 -signkey ~/.ssh/id_rsa -in CSR.csr -req -days 365 -out mycert.crt

Then adding the generated certificate to certifi's (Python module) certificate store as given here. Note that the code in this link adds the certificate without the comments (it literally opens the certificate store file of Python/certifi and adds it) but no worries it works..

Once the certificate issue is sorted, we can now focus on the OAuth2 server setup, client registration and test the OAuth2 access and refresh tokens. The setup is straightforward:
- Just grab the example OAuth2 server code from here
- Even though it has been recently added to the repo, make sure the app.py file contains the flag for refresh token (i.e. 'OAUTH2_REFRESH_TOKEN_GENERATOR': True).

Note here that we are running the https (and thus certificate issues above), we do not care about the variable for disabling https.

Client registration
The client registration follows the steps the example OAuth2 server code example above. Here a couple of important things are :
- Make sure to add "authorization_code" (Authorization code flow) to allowed grant types
- Make sure to add "code" to allowed response types.


Obtaining Refresh Tokens
As mentioned authlib requires the Authorization code flow of Oauth2 in order issue refresh tokens. Just a quick note here on refresh tokens: Refresh tokens are usually long-lived and are used to obtain short-lived access tokens. Some OAuth2 implementations/proposals issue refresh tokens every time an access token is issued. Some others issue only when requested and some others do not support at all. Now coming back to Authorization code flow where an OAuth2 client first requests an authorization code and then uses it to obtain an access and refresh token.  Here is a piece of code taken from authlib's client example page :

client_id = '...'
client_secret = '...'
scope = '...'
session = OAuth2Session(client_id, client_secret, scope=scope)
authorize_url = 'https://127.0.0.1:5000/oauth/authorize'
uri, state = session.authorization_url(authorize_url)

Since we are just testing locally we, the user who would normally be forwarded directed to the link in the "uri" variable, need to open the link and give consent for the the resource referred by the scope. Then the OAuth2 server forwards us to the link that has been given during the client registration with an authorization code and a state parameters. Apparently, authlib can extract the code value from a given url so just do the following as given in the above link

session = OAuth2Session(client_id, client_secret, scope=scope)
urlset = 'https://127.0.0.1:5000/?code=..&state=....'
access_token_url = 'https://127.0.0.1:5000/oauth/token'
token = session.fetch_access_token(access_token_url,authorization_response=urlset)

That's it!!


Ps:
1: Authlib supports also OAuth1, so be careful not to follow the wrong documentation.
2: The documentation suggests that setting an environment variable should allow it to work without HTTPS but I couldn't make it work, let me know if you do :)

On the particularities of brain - body connection

I have been reading a lot about the brain and its workings recently.  It fascinates me how this organ that is 1/50 [1] of our body consumes 25% of our energy and has a neural network with connections more than the number of stars in the galaxy.

What is more interesting for me these days are the behavioural associations between brain or more specifically memory, and the body. Kahneman [2] discusses multiple experiments about this where he shows that the certain memory connections in our brains can be enforced by certain physical activity and the vice versa. For instance thinking about old age (i.e. related concepts) makes us walk slow and doing a physical activity associated with old age makes us recognize words related to old age better.

Then if you look at this TED talk [3] from neuroscientist Wendy Suzuki, this is shown clearly. In fact she switches her research area to connection between physical activity (exercise) and our mental well-being (in all senses). She basically shows that with a personalized physical training we can improve our brain's functionality and prevent the development of brain related diseases in the long-term...

So, what are you waiting for, go and do some physical exercise :))

Stay tuned...  

Refs:
[1] https://en.wikipedia.org/wiki/Brain-to-body_mass_ratio
[2] Thinking, Fast and Slow,  By Daniel Kahneman, 2011
[3] https://www.ted.com/talks/wendy_suzuki_the_brain_changing_benefits_of_exercise#t-734351

Asymmetric (Encryption vs Signing), Digital Signatures and so on...

There is a duality between the use of PKI when performing asymmetric encryption and signing. As very nicely summarized here, encryption (enables one way private communication in case there is only one pair in place) uses the public key to encrypt and private key (there is only one holder) to decrypt, and signing uses the private key to encrypt and public key to decrypt. The former provides more of confidentiality while the latter provides authenticity (origin confirmation), integrity (no modification introduced) and non-repudiation (prevent denial cases : only receiver can open with sender's public key and only from the sender must come because of her private key.

This tutorial is a good one for XML signatures and this tutorial is good to JSON Web signature...
There is also this tutorial on the use of keytool (from Java runtime) to manage keys, certificates, keystores etc...

Stay tuned...

Content Negotiation in Spring Web Applications

Here are some links about the issues related to the use of RequestMapping (PostMapping, GetMapping etc) : Stack Exchange Link

The main issue is when a client (e.g. through Apache HTTP client) sends requests to a servlet with the relevant parameters (here be careful where parameter is posted: in the header or the body, see here and here) the servlet will receive/process the parameters according to a pre-agreement...

Spring framework provides useful functionality and annotations (e.g. PostMapping) to automate/shorten all content negotiation related stuff. See here.

Spring MVC Apps with Eclipse and Maven

If you are not a long time developer of Java servlet applications with Spring tools, it is exhausting to go around and spot what is necessary for developing a dynamic Web application with Eclipse by using Spring MVC. Of course if your application development goes hand to hand with maven development/configuration, it will be great.

Here is a great starter for this (note : based on crunchify tutorial):

- You first create a dynamic Web project in Eclipse (see here) 

- Then you convert the project to Maven project from (right click) Configure/Convert to Maven Project

- Create a Spring configuration file (usually yourproject-servlet.xml). Here you can also use annotation driven view resolving rather than a URL-based. To do that just add "" to your *-servlet.xml file...

- Generate a deployment a descriptor (web.xml) and configure this file. As it is with other servlets this file provides the mapping (among other info) between URLs and servlets. Spring maps the URLs to DispatcherServlet. If you are using Eclipse and started your project as a dynamic Web project, sometimes this file is not generated. But fear not! You can generate a stub file by right clicking your project and choosing Java EE Tools --> Generate Deployment Descriptor Stub ...

- Define your Spring controllers.

- Compiling through Maven : Run as / Maven Build

- Running through Eclipse (make sure you installed Tomcat as a server in Eclipse): Run as / Run on Server.

Good luck.

Ps: This here is also a pretty good reference. 

Bitmasking

This is a good post about bitmasking (efficient way of representing subsets of a set) :
https://www.quora.com/What-is-bitmasking-What-kind-of-problems-can-be-solved-using-it

Hashing Strings with md5 from Linux console

Sometimes, I needed to generate md5 hash of a given string from Linux console. Here is how this can done: echo -n "your text" | md5sum

Stay tuned...

MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [4]

Variable MUSes
An alternative way of explaining inconsistencies in a formula is Variable MUSes (VMUSes) [1]. In plain words, a variable MUS of an unsatisfiable formula F is a subset of variables of F, denoted as Var(F), that defines all variables in an unsatisfiable formula and none of its proper subsets is so. In order to define VMUSes, the concept of induced formula is used. Given a formula F, a formula induced by a variable set V is subformula of F, denoted as F|v, and is the following F|v = {c | c ∈ F and Var(c)}. The set F|v is basically the set of clauses from F, that contains only the variables in V.

By using the notions defined above, a subformula F|v of a given F is said to be a VMUS if the following conditions hold:
- F is UnSAT and V ⊆Var(F)
- F|v is unSAT
- For any V' ⊂ V, F|v' is SAT 

[1] presents two variations of VMUSes:

• Interesting VMUS (IVMUS)
• Group VMUS (GVMUS)

To be continued ...

References
[1] A. Belov, A. Ivrii, A. Matsliah and J. Marques-Silva, On Efficient Computation of Variable MUSes,  SAT 2012.

MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [3]

Coming Back to MUSes and MSSes...
The computation of minimal unsatisfiable subformulas attracted a lot of interest in the recent years. There are several motivations behind this increased interest. First, the complexity (e.g. size) of problems solved by SAT solvers increased a lot recently. For instance, abstraction-refinement model checkers need better abstractions that will help speed up the process. Second, understanding the reasons of conflicts/inconsistencies in a CNF formula requires concise descriptions that are comprehensible by developers. Third, similar to relationship between explanations and relaxations of CSP problems, there is a duality between MUSes and maximally satisfiable subformulas (MSS) and this duality avails the (possible) uses of MSSes. A detailed overview is provided in [1] and [2].

Given a CNF formula F, a minimal unsatisfiable subformula C is a subset of clauses from F (C ⊆ F) that is unsatisfiable and removal of a clause c from C makes C \ {c} satisfiable. The minimum unsatisfiable subformula is one such subformula that has minimum cardinality. The computation of minimum unsatisfiable subformula is given as ∑2-complete in [3]. An important point here related to computation of MUSes from MSSes, in an analogy to computation of explanations from relaxations as discussed in the previous post, is the following from [1]: because computing SAT is in NP (i.e. relatively easy) and UnSAT is CoNP, MSSes are computed first....

However, in general it is not enough to obtain one MUS to explain inconsistencies as there might be many of them. Moreover, the number of clauses contained in a MUS (i.e. inconsistency explanation) can be large leading to a situation the developer can not comprehend or can not understand the reason accurately. Thus several variations of MUS computations have been proposed to make MUSes more concise. I will discuss two of them in here leaving some others to future posts. The first one has been introduced in [1], optimized in [4] and [5]. We will call High-level MUS in what follows. The second one is presented in [6] and we will call it Variable MUS.

High-level MUSes
I am going to discuss High-Level MUSes here with a chronological approach, i.e. towards most recent paper...
[1] In some applications of SAT such as model checking and formal equivalence verification (FEV), MUSes are usually low-level projections (are generated from) of some high-level statements written in a more expressive (and presumably more compact) notation such as first-order logic. Thus one is interested in finding MUSes that are closer to these high-level statements. In order to explain how High-level MUSes are obtained, we first need to explain the concept "selector-variable". A boolean variable v is a selector variable that implies a clause C, v → C (i.e. -v ∨ C). It can be used to enable (by assigning true) or disable (by assigning false) the clause C.

By using selector variables we can identify each clause or group them. In particular, the set of clauses that are associated with the same high-level statement can be marked with the same selector variable. Given a set of clauses {c1,c2,c3,c4} and a set of selector variables F={v1,v2}, consider the following CNF encoding:
-v1 ∨ c1
-v2 ∨ c2
-v2 ∨ c3
-v1 ∨ c4
This encoding can effectively associate {c1,c4} with v1 and {c2,c3} with v2.

[2] focuses on finding one high-level MUS even though the approach can be used for standard MUS extraction. It provides two algorithms: resolution-based MUS extraction and selector-variable based MUS extraction. In general the algorithm first finds a clause-level non-minimal unsatisfiable subformula that contains a part of a projection of an interesting clause (i.e. an equisatisfiable formula obtained by Tseitin transformation) and then tries to squeeze it to minimal. I won't provide the details of algorithms but just present the High-Level MUS definition in the paper. Given a formula F = f1 ∧ f2 ... ∧ fn where each f is a propositional formula and a propositional formula R (called remainder), a high-level MUS, denoted as UC(F,R), imply the following conditions:
- F ∧ R is UnSAT,
- it is a subset of F, i.e. UC(F,R) ⊆ F
- UC(F,R) ∧ R is UnSAT

Here each f ∈ F is called an interesting constraint.

In the next post, I will discuss Variable MUSes...


References:
[1]  Mark H. Liffiton and Karem A. Sakallah, "Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints", Journal of Automated Reasoning, 2008
[2] Éric Grégoire, Bertrand Mazure, Cédric Piette, "On Approaches to Explaining Infeasibility of Sets of Boolean Clauses", 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2008
[3] Anupam Gupta, "Learning Abstractions for Model Checking", PhD Thesis, CMU, 2006
[4] Alexander Nadel, "Boosting Minimal Unsatisfiable Core Extraction", Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design
[5] V. Ryvchinm, O. Strichman, "Faster Extraction of High-Level Minimal Unsatisfiable Cores", Proceedings of the 14th international conference on Theory and application of satisfiability testing (SAT), 2011.
[6] A. Belov,  A. Ivrii, A. Matsliah, J. Marques-Silva, "On efficient computation of variable MUSes", Proceedings of the 15th international conference on Theory and Applications of Satisfiability Testing(SAT), 2011.

MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [2]

Now we start for minimal unsatisfiable subformulas (MUSes) which I categorize unsatisfiability driven as given in the first post. They are sometimes called as minimal unsatisfiable cores in the literature. I believe the research on computing MUSes made the relation between explanations and relaxations (relaxations in short) in CSP research more prominent. I can not say that one triggered/inspired the other as I do not have enough chronological information...

Explanations and Relaxations in CSP
Relaxations[1] are used to explain the reasons (culprits) of inconsistencies and to (optimally) resolve those inconsistencies in over-constrained CSP problems. Given a CSP problem with a set of user constraints C and background constraints B (hard constraints),  explanations and relaxations are sets of constraints CE ⊆ ℘C and CR ⊆ ℘C respectively. An explanation R ∈ CE is (subset) minimal if the following conditions hold:

• R = {ci, ... , cn} is unsatisfiable 
• Removal of a constraint c from R is satisfiable, i.e. R \ {c} is consistent.

Notice that a subset minimal explanation is not cardinality minimal explanation. A cardinality minimal explanation is a subset minimal explanation that the minimum number of constraints. A relaxation R ∈ CR is a maximal relaxation if the following conditions hold:

• R = {ci,...,cn} is satisfiable 
• Addition of a constraint c to R makes the formula unsatisfiable, i.e. let c ∉ R, the formula R ∪ c is inconsistent.

In very short terms, the relation between explanations and relaxations is the following: the complement of each hitting set of all minimal relaxations is one maximal relaxation. A constructive way of computing explanations is to check the consistency of B ∪ C and iteratively remove one constraint until an unconsistency is obtained. Thus relaxations are computed first. More details are available at [1].

We stop here with CSP explanations and relaxations and start with SAT MUSes in the next post...


References:
[1] Ulrich Junker, "QUICKXPLAIN: Preferred Explanations and Relaxations for Over-Constrained Problems", Proceedings of the Nineteenth National Conference on Artificial Intelligence (AAAI), 2004

MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [1]

I have been recently reading a lot about computation of some satisfiable/unsatisfiable subformulas from a given CNF SAT formula. There are many different problem definitions that represent these computations (respective subformulas). I will try to summarize all of them to the extent of my knowledge while trying to give some usecases and respective references. I am going to start first with satisfiability driven subformula computations. The available solvers may be considered as satisfiability-based, unsatisfiability-based or some other techniques [1,3]...

The general name of computing maximum number of satisfiable clauses from a given formula F is MaxSAT. In MaxSAT, we try to find a subset of clauses C  ⊆ F such that the followings hold:

• C is satisfiable
• There is no other satisfiable subset C' ⊆ F such that |C'| > |C|.

Notice that if F is satisfiable then C = F. Depending on the problem that F encodes, several MaxSAT variants have been proposed. I will discuss two of them: Partial MaxSAT and Weighted MaxSAT. In partial MaxSAT we have soft clauses (relaxable) and hard clauses (non-relaxable). A PMaxSAT solver tries to find the maximum number of satisfiable soft clauses while making sure hard clauses are satisfiable. According to MaxSAT'13 competition a PMaxSAT CNF is specified as : "p wcnf nbvar nbclauses top"[2] where nbvar is the variable number, nbclauses is the number of clauses and top is the weight of hard clauses. Soft clauses have the weight of 1. Example:
p wcnf 3 3 8
1 -1 2
1 -1 3
8 1 2 3

Weighted MaxSAT associates each clause with a weight that is greater than or equal to 1. A WMaxSAT solver tries to find a subformula that has the maximum sum of weights of clauses that are satisfiable (Note here: I think Wiki definition is a bit misleading here...). With weighted MaxSAT one can introduce an ordering between clauses (and thus the high level problem components). There is also a variant in which there are hard clauses. This is a slightly different version of partial MaxSAT with soft clauses having variable weights.

MaxSAT is an active area of research so different variants are proposed every now and then. Many efficient techniques have been/are proposed already...

Stay tuned...
 

References :
[1] http://en.wikipedia.org/wiki/Maximum_satisfiability_problem
[2] http://maxsat.ia.udl.cat/requirements/
[3] T. Alsinet, F. Manya, J. Planes, "Improved Exact Solvers for Weighted Max-SAT",  In Proceedings of Eighth International Conference on Theory and Applications of Satisfiability Testing 2005. NOTE for this paper : For instance, a MaxSAT solver may try to find a truth assignment that minimizes the sum of weights of unsatis ed clauses

Latex (Tex live) update on Macosx

I recently had a problem with my Latex distribution. I was missing a package and as you may probably know, there are so many Tex distributions and it is difficult to keep up-to-date the installation. Updates work for a year and then you need to install tex distribution once more if you want to get new packages that were not there or updated for the new distribution. In these cases, manual installation could be helpful... What I did for manual installation:
- Copied the .sty file to /usr/local/texlive/2010/texmf-dist/tex/latex  (note that this may change in your system)
- Ran texhash (with sudo).

Good luck...

Two's complement, bitwise operations, old school info:)

When I was playing with a Java library, I realized that I need to refresh some prehistoric information. The bitwise operations in Java :
http://www.leepoint.net/notes-java/data/expressions/bitops.html

Then I found myself looking integer representations in binary formats (4Bytes) that are useful to understand the effects of bitwise operations:
http://en.wikipedia.org/wiki/Two%27s_complement

Stay tuned...

Why my "touch" lights works without touching?

I have a nice touch light that I had bought some time ago. It works with a simple voltage change logic but recently started switching automatically (better to say unexpectedly). I started googling whether there are some other people having the same problem and I found out it is a well known problem.
Here is one of the useful links : 
http://boards.straightdope.com/sdmb/showthread.php?t=551416

I hope you also find it useful.

Passing command line arguments to MacOSX Applications with GUI and more

Several days back, I was working on a Latex document by using Texworks. The people who used Texworks would know that it is quite useful editor with simple but smart features. One of the main drawbacks of Texworks is (perhaps it is the same for most of Latex editors) it is quite difficult to configure the colors of various components such as background. Background color is quite important as it covers most of the editor surface (and so effects the eyes)... \\

From that point I started looking for ways of changing background color of Texworks and came by this link here : http://www.latex-community.org/forum/viewtopic.php?f=56&t=6921
It explains how to modify the background color of Texworks (which is a Qt application) by playing with some qt parameters... But I had to pass the parameters (i.e. CSS file) to Texworks from command line (which is an Application in my MacOSX). Then I found this link which explains a very simple way of doing it : http://hints.macworld.com/article.php?story=20080809181956219

That didn't finish the story yet :) Then I started pondering around the colors, their effects on us... Which colors are more relaxing, disturbing, natural etc etc. Here is a good link that discusses the issue. It seems the tones of green and blue are more relaxing...

Stay tuned.

Simple image processing with Java

Java has a rich set of libraries for manipulating images. I just use very basic features for the time being and I wanted to put a note here for the newcomers like me. To my understanding, Java uses a protocol when loading a resource (url = getClass().getResource(fileName)) and images "should" be considered as resources (ImageIO.read(url)). Of course there can be other ways of doing it but here is a summary to load resources to Java projects in Eclipse and a piece of code to play with images in Java:
1. http://stackoverflow.com/questions/8960381/runnable-jars-missing-buttons/9278270#9278270
2. http://www.coderanch.com/t/338329/GUI/java/draw-lines-without-change-background

Stay tuned ...

Four key factors in food selection

I recently got a present book from a very "sweet" person in my life. As you can understand from the way I describe the person who gave it to me the book is about foods. It is called "The 150 Healthiest Foods on Earth". I started reading the book and at the very beginning, it came a very important point where four main factors used in the quality rating of foods are listed. I just wanted to list them in this entry:
- Omega-3 fats
- Fiber
- Antioxidants
- Glycemic index

Changing Background Color of an Image in GIMP

Recently I needed to use a simple picture in my presentation. However, the picture had its own background color which was annoying for the presentation template. What I did is the following:
1. I opened the picture in GIMP.
2. There is a nice set of selection tools in GIMP. I used scissor selection tool to choose the relevant parts of my picture.
3. Pasted the selected tool to a new file without background color...

That is it. There is a nice tutorial about the subject here: http://docs.gimp.org/en/gimp-tool-foreground-select.html

Deforestation and dynamic world forest coverage view

It is sad that the deforestation is still a problem despite the global awareness of environmental concerns. I was caught up with the fact that Ireland, a country that continuously gets rain, has relatively very small forested area. Starting from this point, I came by this link and I wanted to share...

http://www.guardian.co.uk/environment/interactive/2007/dec/13/forests

Youtube repeated

Today I discovered an interesting link for listening (watching would make less sense) Youtube repeatedly :http://www.youtuberepeat.com The idea is quite simple but smart :)