A prop P is a symmetric monoidal category whose objects are the non-negative integers, with tensor product defined as addition of integers (so morally, it's a single object V, the unit object, and various powers of V; so it's the morphisms that make it interesting). A representation of prop P in a symmetric tensor category C is a symmetric tensor functor from P to C.

A prop is a way of encoding the morphisms defining a structure you are interested in, in a universal way. A representation of a prop P in a category C is then the same thing as a gadget modelled by P, in the category C. For instance see the prop Alg below; it's representations in C are the same thing as algebras in C. One nice thing about Props is that they can be given by generators and relations, and also they express via Schur functors $\mathbb{S}_\lambda$ defined in any symmetric tensor category similarly to the definition in $GL_n$ (if someone wants I can elaborate, but a search for Schur functors will probably yield enough results).

Examples include the prop "Alg": it has a morphism $u:1\to V$, and a morphism $\mu: V\otimes V\to V$, and a relation $\mu\circ(\mu\otimes id)=\mu\circ(id\otimes \mu)$, and a relation $\mu(u\otimes id)=\mu(id\otimes u)=id$, etc. So you formally take the symmetric tensor category on objects the non-negative integers, which admits maps like $\mu$ and $u$, and you quotient by those relations. One can similarly define Lie-Alg, Lie-Bialg, Bi-alg, Hopf, quasi-Hopf,... you can go all day.

A key point is that morphisms between props induce pullback functors between their representations in any symmetric tensor category, but in the reverse order (meaning, as usual $\rho:P\to S$ induces $\rho^*:S-mod\to P-mod$. For instance, there is a morphism of props from Lie-Alg to Alg, sending the bracket $[,] \mapsto m - \tau\circ m$. This induces the familiar forgetful functor from Alg to Lie-alg.

In situations where there is a quantum structure that is a quantization of a classical structure, you get two props defined over $k[[\hbar]]$. For example in the case of Lie-Bialg, and Hopf alg, both of these make sense over k[[\hbar]]. The classical limit functor is induced by a prop map from Bialg to Hopf alg. It turns out to have a section Hopf alg to Bialg, which is the sort of thing you can check by generators and relations. Of course it doesn't have a unique section, there are many choices. However, the fact that you make those choices ONCE and FOR ALL on this particular prop, then implies that you have a functor of quantization between these two structures in any symmetric tensor category. I think a moral is that asking some construction in symmetric tensor categories be functorial, which is in general a tricky business, can in certain instances be reduced to giving a single (not even necessarily canonical!) map of props.

In the case of Kontsevich quantization, The problem seems to be that quantizations are classified (up to isomorphism!) by HH^2(M) (if it's a Poisson manifold), and HH^2(A,A) of the algebra in general. Obstructions to quantization appear in HH^3. If, for instance HH^3(A,A) vanishes, it means you can quantize your Poisson algebra step-by-step. You basically start with your two-cocycle, it gives you a first order deformation, you try and see if your new algebra structure is associative so far (meaning write down associativity identity, expand in power of $\hbar$, and examine the first place where it isn't trivially zero); this will yield a certain very explicit 3 co-cycle which you need to vanish. If that 3-cocycle vanishes in HH^3, then you get it as d(w) for some 2 co-cycle. This then gives you the next higher order deformation of the multiplication, on and on ad infinitum.

The problem here is that at each step you are making a choice of cocycle w such that dw=your previous obstruction. The results you get will be unique up to some non-canonical isomorphism, but that isn't good enough for functoriality. In particular, there is not a prop morphism between non-commutative algebras and Poisson algebras which would unify the approach for all examples.