Yes this is correct. A modal statement "it is possible that P" has a truth value that need not be that of P, because the latter depends on whether P obtains in the actual world, whereas the former depends on whether P obtains in at least one possible world.
Note though that possible world semantics is just a way to analyse modal statements. One must distinguish the semantics (a mathematical construction that represents what a statement is talking about) and the syntax (the form and construction rules of statements). Modal statements usually don't refer to specific worlds, they only contain "possible" and "necessary" operators, so I would have framed the question differently without mentioning specific worlds.
For example, your contradiction example could be "it is possible that P and it is necessary that not-p", which is contradictory.
There are indeed proofs in modal logic. You can either use deduction proofs using the axioms of modal logic (there are different axioms associated with different systems, but a common base) or natural deduction rules. Truth tables are the semantics of non-modal logic. Since the semantics of modal logic is different, you cannot use them: you need a possible world semantics.
Your two examples are as you say: the first is a logical truth and the second a logical contradiction. You don't even need to interpret the modal operator to know that, and you could have constructed contradictions that are specific to modal logic (such as <>p <=> []~p or p^[]~p)
Finally, modal statements have a truth value as a matter of logic, but it is more contentious whether or not they have a truth value as a matter of metaphysics (whether they correspond to something in the world). This depends on the kind of modality involved (nomological necessity, metaphysical necessity...), and some authors deny that they have truth values: they would be a mere way of talking.