What properties are allowed in comprehension axiom of ZFC?

To formalize a property of a set simply means to give a formula in the language of set theory. That is $\phi(x)$ is nothing but a formula in the language.

Now, for each such property of sets $\phi(x)$ there is an axiom that says that given any set $A$ the set $\{x\in A\mid \phi(x)\}$ exists. This is the axiom schema of specification. Russele's Paradox does not creep in here since you still can't form the set $\{x\mid x\notin x\}$ not since you can't formulate the property $\phi(x)=x\notin x$ (you certainly can) but simply since using the axiom schema of specification will only allow you to create such sets as $\{x\in A\mid x\notin x \}$. By the axiom of foundation this set is just $A$.

As mentioned above, by "$\varphi(u)$ formalizes a property of sets" we just mean that $\varphi(u)$ is a formula in the language of set theory. Fortunately, virtually all of mathematics can be formalised within the language of set theory, and so as long as you stick with mathematically meaningful properties, you can use Comprehension to construct subsets of any given set. Unfortunately, Comprehension could not allow you to construct the set of all happy horses (until you have given a mathematically meaningful definition of a happy horse).

The ZFC axiomatization side-steps the issue of Russell's paradoxical set (as opposed to simply outlawing its formation as was done in the Russell theory of types, and Quine's New Foundations).

It is done in the following manner: Naive set theory may be thought of as essentially axiomatizaed by the Axiom Schema of Unrestricted Comprehension:

For any formula $\varphi (u)$ (with no free occurrences of the variable $y$), the universal closure of $$( \exists y ) ( \forall u ) ( u \in y \leftrightarrow \varphi (u) )$$ is an instance of Unrestricted Comprehension.

(We disallow free occurrences of $y$ in $\varphi (x)$ so that this new set isn't defined as the collection of all objects in some relation to this heretofore undetermined set; otherwise we could take $\varphi (x) \equiv x \notin y$, and get a different paradoxical set: $y = \{ x : x \notin y \}$.) That is, for any set theoretic property $\varphi(u)$ that you can think of, there is a set whose elements are precisely all those objects $u$ satisfying $\varphi (u)$. As an example, there is a universal set, given by taking $\varphi(u) \equiv u = u$: $$V = \{ u : u = u \}.$$ Russell's paradoxical set is given by the formula $\varphi (u) \equiv u \notin u$: $$R = \{ u : u \notin u \}.$$

ZF(C) takes the stance that we cannot use Comprehension to demonstrate the existence of inherently new sets, but only the existence of sets which are definable subsets of already given sets:

For any formula $\varphi (u)$ (with no free occurrences of the variable $y$), the universal closure of $$( \forall x ) ( \exists y ) ( \forall u ) ( u \in y \leftrightarrow ( u \in x \wedge \varphi (u) ))$$ is an instance of Comprehension.

Let us naively try to use Comprehension to get Russell's paradoxical set. Given any set $X$ we may form the set $$X^\prime = \{ u \in X : u \notin u \}.$$ However, if it happens that $X \notin X$, then $X \notin X^\prime$ (since $X^\prime$ only contains elements of $X$), but $X$ itself is a set which would be an element of Russell's paradoxical set $R$. So for any set $X$ which does not contain itself as an element, the associated $X^\prime$ cannot be Russell's paradoxical set. As luck would happen, another axiom of ZFC (the Axiom of Regularity) immediately implies that no set contains itself as an element, which then implies that we cannot use the Axiom of Comprehension with the formula $\varphi(u) \equiv u \notin u$ to prove the existence of Russell's paradoxical set.

Note that because of Regularity under ZF(C) we have $R = V$, and it can easily be shown that ZF(C) proves that $V$ is not a set: if $V$ were a set, then by definition $V \in V$, contradicting Regularity!

Of course, ZF(C) could turn out to be inconsistent, and would then prove the existence of Russell's paradoxical set (and still also disprove its existence). Life would be easier if we could determine exactly which formulas are unproblematic in applications of Comprehension (or Replacement), but life isn't always easy.